Pith. sign in

REVIEW 4 major objections 4 minor 63 references

Generative Compilation: On-the-Fly Compiler Feedback as AI Generates Code

T0 review · 4 major / 4 minor · reviewed 2026-08-02 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read A lightweight 'sealor' completes partial programs so an off-the-shelf compiler can check them mid-generation, turning the compiler into an on-the-fly diagnostic for LLM code generation and reducing Rust compile errors relative to post-gener

desk verdict A solid, original paper with real results; the Rust sealor's informal completeness is the main gap, but the empirical case holds. read the letter →

arxiv 2607.13921 v2 pith:4LBVAAZT submitted 2026-07-15 cs.PL cs.AIcs.LG

Niels Mündler-Sasahara , Hristo Venev , Dawn Song , Martin Vechev , Jingxuan He This is my paper · ORCID
classification cs.PLcs.AIcs.LG
keywords generativecompilationsealorpartialprogramscompilerfeedbackRustLLMcodegenerationprefixcheckingconstraineddecoding
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper's aim is to make compiler feedback available while code is being generated, not only after a file is complete. Its central proposal is generative compilation: wrap a standard compiler with a sealor, a lightweight pass that turns a partial program into a complete one by filling missing syntax and inserting well-typed placeholders, so the compiler's verdict applies to the prefix. The paper proves that on a core Rust-like calculus the sealor is globally complete—no prefix that can be completed to a valid program is ever rejected—with the proof mechanized, and it extends the same design to real Rust, where type and borrow checking are delegated to the existing compiler. In evaluations on repository-level Rust tasks across seven models, this mid-generation feedback lowers the compiler-error rate from 20.7% to 13.1% compared with standard post-generation feedback and improves functional correctness in most model-task settings. The reason to care: if right, it turns the compiler from a gate at the end of generation into an active participant in generation, usable with black-box models and existing infrastructure.

What carries the argument

The central device is the sealor, a transformation from partial programs to complete programs. It preserves already-generated syntax, fills in missing structure, and inserts two placeholders: a diverging one (so control-flow branches impose no typing obligations on the live side) and a generic value-producing one (so value positions can be closed without disabling the borrow checker). The sealor's completeness and soundness are shown to lift to the induced generative compiler whenever the underlying compiler is exact.

What would settle it

Run the released Rust sealor over every prefix of a large corpus of valid and near-invalid Rust files—truncate each file at every token boundary and seal the prefix. If any prefix that has a valid completion is rejected after sealing, or any prefix that has no valid completion is accepted, the practical completeness/soundness claim is false; a single counterexample suffices.

Watch

Extended reading notes

Core claim

The paper's central claim is that a compiler can be made to reason about incomplete programs by a lightweight, mostly syntax-guided transformation called a sealor. A sealor takes the prefix of a program as it streams out of an LLM, fills in missing syntax, and inserts well-typed placeholders—a diverging placeholder for control-flow branches and a generic value placeholder for value positions—so that an off-the-shelf compiler can run on the result. The design targets two properties: global completeness, meaning any prefix that has a valid completion is never rejected, and selective soundness, meaning the sealor also rejects a meaningful class of dead ends early. The paper proves global comple

Load-bearing premise

The practical sealor's rules assume that for every Rust construct, sealing preserves the existence of a valid completion; this is argued feature-by-feature informally for real Rust and lifts the formal guarantee only under an idealized exact compiler, so one counterexample in a single construct would invalidate the practical completeness claim.

Editorial extensions

If this is right

  • LLM coding loops gain a prefix checker with rich, compiler-style diagnostics, without white-box token access or reimplementation of the language's type system.
  • Because a rejection triggers regeneration rather than token filtering, a false rejection costs a prefix while a missed dead end is still caught later; this is why the approach prioritizes completeness over soundness.
  • Error reports become smaller and more focused: on the evaluated tasks, the average diagnostic count drops from 13.8 to 5.5, and errors are typically reported near their source rather than at file end.
  • Many tasks complete without ever needing a post-generation check (85.3% of the paper's runs), and the approach composes with ordinary post-generation feedback when needed.
  • The compiler becomes a first-class participant in AI-assisted programming, active during generation rather than only a final gate.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The sealing idea is language-agnostic in principle, so it should transfer to other strict languages; the bottleneck is hand-deriving completeness-preserving rules for each construct, suggesting automated sealor synthesis as a next step.
  • Completeness is proven for the core calculus, not for real Rust; the practical checker's guarantee rests on informal per-feature arguments, so a stress corpus of valid-but-odd Rust prefixes would clarify how far the guarantee actually extends.
  • Because soundness is deliberately selective, there is room to push the sealor further: using expected types from context could catch more dead ends before generation ends without breaking completeness.
  • The paper observes empirically that diagnostics reflect genuine defects rather than sealing artifacts, but does not prove it; formalizing that link would strengthen any use of these diagnostics as a training signal.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 4 minor

Summary. The paper introduces generative compilation, a method that obtains compiler feedback on partial programs during LLM generation. The core device is a 'sealor' that transforms a partial program into a complete program that an off-the-shelf compiler can check. The authors formalize sealor completeness and soundness in a generic framework, instantiate it on Featherweight Rust (FR) with a syntax-guided sealor, and report that the full FR development—including the sealor's global completeness and selective soundness—is mechanized in Lean. They then describe a sealor for real Rust that delegates semantic checking to rustc while using placeholders (holeval() and holediv()) and targeted error suppression. The evaluation on repository-level C-to-Rust translation and updated-API tasks across seven LLMs reports that generative compilation reduces the compiler error rate from 20.7% (post-generation feedback) to 13.1% and improves functional correctness in 11 of 14 model-task configurations.

Significance. If the claims hold, this is a novel and practically relevant contribution: it reuses existing compiler infrastructure, works with black-box LLMs, and provides diagnostics during generation rather than only after completion. The formal FR development is a substantial strength, especially since it is machine-checked in Lean and the authors release the mechanization, implementation, and benchmark. The reported empirical gains are meaningful and the analysis of early error detection is informative. However, the central practical claim—that the real-Rust sealor is a sound basis for on-the-fly feedback—rests on informal per-feature arguments rather than a mechanized or otherwise rigorous completeness argument, and the diagnostics that are the method's main advantage are explicitly not formalized. These gaps are load-bearing for the practical contribution, so the paper needs significant strengthening before it can be accepted.

major comments (4)
  1. [§6.2, §6.1] The real-Rust sealor's global completeness is not established. The paper states in §6.2 that it gives 'informal, per-feature arguments for typing behavior, completeness, and soundness, rather than the formal, mechanized treatment we gave for the whole FR,' but Theorem 3.2's lifting result requires a complete sealor. A concrete completeness risk is the expression sealor's insertion of holeval(), whose type parameter T is resolved by inference. §6.1 says E0282 ('type annotations needed') is suppressed only inside partial function bodies, yet holeval() is used in arbitrary expression contexts—e.g., a partial closure body or an if/else branch whose expected type is not yet constrained by later code. If such a context triggers E0282, the sealor would reject a prefix that admits a valid completion, breaking the 'never reject completable prefixes' guarantee and sending spurious feedback to the
  2. [§5.3, Theorem 5.3] The proof of global completeness for arbitrary strings silently relies on the lemma that every prefix of a well-typed FR term parses to a partial term in Fig. 9. This is stated in the proof ('parsing s yields a partial term b_t') but not proven or cited as a mechanized lemma. The property is not immediate for arbitrary token boundaries (e.g., partial identifiers, partial keywords, and whitespace), and it is exactly what lifts completeness from partial-syntax terms to the arbitrary-string setting of the main theorem. If this lemma is included in the Lean mechanization, the paper should point to it explicitly; otherwise it must be stated and proved.
  3. [§5.4, Lemma 5.4 and Theorem 5.5] The selective soundness result at statement boundaries is nearly tautological. Lemma 5.4 shows that for every b_t in X_stmt, b_t realizes S_FR(b_t); Theorem 5.5 then follows immediately from the well-typedness of the sealed term without any additional reasoning about alternative realizations. In other words, the soundness direction holds because the sealor's output is itself a completion of the boundary prefix. This does not provide a nontrivial characterization of when rejection at a statement boundary corresponds to a genuine dead end. The paper should either strengthen this result or temper the claim that the sealor 'correctly flags an important class of partial programs with no valid extension.'
  4. [§8] The paper explicitly states that the formal completeness and soundness results 'concern only ok, and do not model err,' and that formalizing whether err describes a genuine defect in the original partial program is future work. Since the distinguishing advantage over constrained decoding is precisely the availability of compiler-style diagnostics, this is a significant gap between the formal framework and the practical mechanism. At minimum, the paper should state a clear correctness criterion for diagnostics (e.g., no diagnostic is caused solely by sealing-inserted code) and provide evidence beyond aggregate error rates that the projected diagnostics are not misleading. The current empirical analysis of diagnostic delay and error kinds is suggestive but does not directly test diagnostic fidelity.
minor comments (4)
  1. [§6.1] The notation for holeval() is written as 'const fn holeval()<T>()→T', which is not valid Rust syntax; it should be 'const fn holeval<T>() -> T'. Please clarify.
  2. [§6.2] The block-sealor rules are hard to read as typeset; for example, 'b_b ::= { s; e? }' and the partial-block rows appear to be missing semicolons or separators. A cleaner presentation of the partial syntax and the sealor rules would help.
  3. [§7.1, Table 1] The table reports percentages without sample sizes or confidence intervals. The text mentions a paired difference test at α=5%, but the test is not described in the main text or appendix. Please provide the number of instances per task and a brief description of the significance test.
  4. [§7.3] The definition of GC_fn is informal ('a simpler variant that checks only completed function bodies'). Since Fig. 12b and Fig. 12c compare against it, please specify this baseline precisely so the comparison is reproducible.

Circularity Check

0 steps flagged · score 1.0 of 10

No load-bearing circularity: the FR formal results are derived from stated definitions and mechanized in Lean; the real-Rust completeness gap is an unverified assumption, not a circular step.

full rationale

The central derivation chain is self-contained rather than circular. Theorem 3.2 is a direct implication from the definitions of sealor completeness/soundness and compiler exactness, with the proof given in the paper. The FR results (Theorems 5.1-5.3, 5.5-5.7) are proved by syntax-directed induction over the partial-term grammar and are claimed to be fully mechanized in Lean, so they do not reduce to a fitted parameter or to the paper's own empirical claims. The statement-boundary soundness proof is direct because the sealor's output realizes the partial statement, but exhibiting the sealor's own output as the witness is a valid proof step, not a hidden reduction of the kind that would make the result definitionally equivalent to its input. The real-Rust sealor's completeness is explicitly left informal: §6.1 says 'we give informal, per-feature arguments for typing behavior, completeness, and soundness, rather than the formal, mechanized treatment we gave for the whole FR,' and §8 notes that diagnostics are not formalized. These are genuine limitations and correctness risks—for example, holeval() inserted in an underconstrained expression context could trigger E0282 and cause a spurious rejection—but an unproved property is not circularity. The evaluation compares against external benchmarks (CRUST-Bench and a constructed API-update set) and no parameter is fitted to the reported error-rate reduction. The self-citations [31], [33], and [54] are peripheral: [31] is cited for standard prefix-checker vocabulary and for the claim that type-constrained decoding reimplements typing, not as a uniqueness theorem or as the basis of the sealor construction. No ansatz is smuggled in via self-citation, and no known result is merely renamed. Overall, the paper's derivation is independent of its conclusions; only minor self-citations are present, so the score is low.

Assumptions & free parameters 3 free parameters · 4 assumptions · 3 invented entities

The central claims rest on the exactness of the compiler, coverage of the partial syntax, and the informal completeness arguments for real Rust. The free parameters are experimental budget choices, not fitted coefficients. The invented placeholders and the sealor itself have falsifiable handles in the implementation and tests.

free parameters (3)
  • early-feedback restart budget k = 10
    Hand-set threshold for the number of on-the-fly restarts; sensitivity is ablated in §A.5 but the choice affects the reported improvements.
  • total feedback iterations n = 15 (UpdatedAPI), 20 (Translation)
    Hand-set budget for total feedback rounds; affects both PC and GC equally but bounds the observable gains.
  • sampling temperature = 0.6
    Sampling hyperparameter for LLM evaluation; Opus uses provider default. Not central to the sealor claim.
assumptions (4)
  • domain assumption The compiler C is exact for the target language (sound and complete).
    Theorem 3.2 lifts sealor guarantees only if C decides L exactly; for rustc this is an idealization (bugs, unstable features).
  • ad hoc to paper Every prefix of a well-typed FR program parses to a partial term in Fig. 9.
    Used in Theorem 5.3 to move from partial-syntax completeness to arbitrary strings; the proof states 'parsing s yields a partial term b_t' without formal proof.
  • domain assumption Pearce's FR type and borrow safety hold for the corrected typing rules.
    The paper relies on FR soundness after making corrections; the Lean mechanization is claimed to re-establish it.
  • domain assumption rustc's behavior conforms to the per-feature sealing rules (completeness of each rule).
    For real Rust, no mechanized connection exists between sealing and rustc semantics; the paper relies on rustc's inference as an oracle and suppresses selected errors.
invented entities (3)
  • holeval() independent evidence
    purpose: Generic well-typed value placeholder that does not diverge at the type level, used to seal expression positions without disabling borrow checking.
    Introduced in §6.1; implemented as const fn holeval<T>() -> T { panic!() }; its behavior is verified by the shipped tests and by rustc's type-checking of sealed programs.
  • holediv() (panic!()) independent evidence
    purpose: Diverging placeholder for control-flow branches so rustc does not require later code to type-check after it, preserving completeness.
    Same section; uses the never type's coercion to any type; shipped implementation uses panic!().
  • sealor S independent evidence
    purpose: Core transformation converting partial programs to complete ones for compiler checking; the concept is the paper's central contribution.
    Formally defined for FR and installed for Rust; evidence is the claimed Lean proofs and the empirical evaluation.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Generative Compilation: On-the-Fly Compiler Feedback as AI Generates Code." pith.science (2026). https://pith.science/paper/4LBVAAZT

@misc{pith2026260713921,
  author       = {Pith},
  title        = {Pith review of: Generative Compilation: On-the-Fly Compiler Feedback as AI Generates Code},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/4LBVAAZT}},
  note         = {Machine review of arXiv:2607.13921}
}
read the original abstract

Languages with rich static semantics, such as Rust, provide stronger guarantees for AI-generated code, but their strictness makes generation more difficult. Off-the-shelf compilers can provide useful feedback post-generation, but does not guide intermediate generation steps, such as those during autoregressive LLM decoding. Constrained decoding intervenes earlier by rejecting invalid tokens during sampling, but requires white-box model access and costly reimplementation for semantic constraints. We introduce generative compilation, the first approach to obtaining compiler feedback on partial programs during generation. The core technical device is a sealor: a lightweight, mostly syntax-guided transformation that converts partial programs into complete ones that standard compilers can diagnose. It is designed such that possible-to-complete partial programs are never rejected, while preserving enough code context to catch genuine dead ends early. We construct such a sealor on a core Rust-like calculus and prove that it satisfies these properties, all mechanized in Lean. We extend it to the first partial-program checker for real Rust. We evaluate our method on challenging repository-level Rust coding tasks, across both frontier black-box and open-weight models. We show that generative compilation reduces non-compiling outputs and improves functional correctness, relative to standard post-generation feedback. It does so by detecting a broad range of errors close to their source and early during generation, thereby reducing errors cascades and enabling focused diagnostics. More broadly, generative compilation is a step toward making compilers a first-class citizen of AI-assisted programming active during generation, rather than a separate post-generation check.

Figures

Figures reproduced from arXiv: 2607.13921 by the authors.

Figure 1
Figure 1. Non-compilable LLM-generated Rust code. Given a prompt 𝑥 (a natural-language task, op￾tionally with reference code) and the code gen￾erated so far 𝑐, 𝑀 produces a next-token distri￾bution 𝑀(· | 𝑥 ◦ 𝑐), where ◦ denotes string con￾catenation. A token 𝑡 ∼ 𝑀(· | 𝑥 ◦ 𝑐) is sampled, appended to 𝑐, and generation repeats until a special end-of-sequence token EOS is produced. As discussed above, this process can generate an… view at source ↗
Figure 2
Figure 2. Error message returned by the Rust compiler after it rejects the program in Fig. [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. The regenerated Rust program above compiles [PITH_FULL_IMAGE:figures/full_fig_p004_3.png] view at source ↗
Figures from the paper (16 more)
Figure 4
Figure 4. Figure 4: Constrained decoding rejects . as it leads to a dead-end program prefix. Assume for now that a (well-implemented) constrained decoding engine for Rust is avail￾able, and let us again examine the example pro￾gram in [PITH_FULL_IMAGE:figures/full_fig_p005_4.png]
Figure 5
Figure 5. Figure 5: A full Rust program produced by our sealor. [PITH_FULL_IMAGE:figures/full_fig_p006_5.png]
Figure 6
Figure 6. Figure 6: We combine generative compilation and LLM-based code generation as two (concurrent) modules. [PITH_FULL_IMAGE:figures/full_fig_p008_6.png]
Figure 7
Figure 7. Figure 7: FR’s Syntax, following Pearce [41]. 4 FR: A Core Calculus for Rust In this section, we review Featherweight Rust [41], a compact calculus inspired by Rust’s borrow system. We present the syntax (§4.1) and typing (§4.2) needed to demonstrate our generative compilation a…
Figure 8
Figure 8. Figure 8: FR’s typing rules for terms [41]. Grey boxes highlight corrections made by our mechanization. was declared. The store typing 𝜎 assigns types to runtime locations. 𝜎 is needed only when typing intermediate execution states; source-level programs are typed under 𝜎 = ∅. T…
Figure 10
Figure 10. Figure 10: Our realization relation for FR terms (b [PITH_FULL_IMAGE:figures/full_fig_p013_10.png]
Figure 11
Figure 11. Figure 11: Our syntax-guided sealor SFR [PITH_FULL_IMAGE:figures/full_fig_p014_11.png]
Figure 12
Figure 12. Figure 12: Our analysis on the effects of generative compilation ( [PITH_FULL_IMAGE:figures/full_fig_p024_12.png]
Figure 13
Figure 13. Figure 13: The error kinds detected during rollbacks span syntax errors, type errors, borrow-check and lifetime [PITH_FULL_IMAGE:figures/full_fig_p032_13.png]
Figure 14
Figure 14. Figure 14: Fraction of compilable outputs by restart [PITH_FULL_IMAGE:figures/full_fig_p032_14.png]
Figure 15
Figure 15. Figure 15: End-to-end excerpt from a GC run by Claude Opus 4.8 on the rustls-webpki API-update task. The partial output borrows from a temporary CertificateDer and is rejected with E0716. After receiving the diagnostic, the model introduces the longer-lived trust_anchor_cert bin…
Figure 16
Figure 16. Figure 16: Instruction appended to the user message when inference is run with an empty initial assistant [PITH_FULL_IMAGE:figures/full_fig_p035_16.png]
Figure 17
Figure 17. Figure 17: Feedback message used by Generative Compilation. The prompt history first receives the rejected partial assistant output {prefix}{code}, followed by this user message with rendered compiler diagnostics. Your previous output was rejected by the compiler. Compiler error…
Figure 18
Figure 18. Figure 18: Feedback message used by Post Compilation. The prompt history first receives the rejected complete assistant output, followed by this user message with the rendered compiler diagnostics. The model may respond with full replacement files, patches, or a combination; the…
Figure 19
Figure 19. Figure 19: User prompt for UpdatedAPI. The model receives the crate files, including tests and comments, and is asked to implement only the incomplete interface file; {interface_path} is instantiated with src/lib.rs. The trailing prefix instruction replaces the prefilled assista…
Figure 20
Figure 20. Figure 20: User prompt for Translation. It gives the C sources and the incomplete Rust interface of the target file. The trailing prefix instruction replaces the prefilled assistant answer for black-box models (§C.1) [PITH_FULL_IMAGE:figures/full_fig_p037_20.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

63 extracted references · 2 linked inside Pith

  1. [1]

    Agrawal, Aditya Kanade, Navin Goyal, Shuvendu K

    Lakshya A. Agrawal, Aditya Kanade, Navin Goyal, Shuvendu K. Lahiri, and Sriram K. Rajamani. 2023. Monitor-Guided Decoding of Code LMs with Static Analysis of Repository Context. InNeurIPS

    2023

  2. [2]

    Rajeev Alur, Rastislav Bodík, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. 2013. Syntax-guided synthesis. InFMCAD

    2013

  3. [3]

    Anthropic. 2026. Claude Opus 4.8 System Card. https://www-cdn.anthropic.com/ 0f0c97ad20d8005706296bd92aa1c27c6b2f4f61/Claude%20Opus%204.8%20System%20Card.pdf

    2026

  4. [4]

    Luca Beurer-Kellner, Marc Fischer, and Martin Vechev. 2024. Guiding LLMs The Right Way: Fast, Non-Invasive Constrained Generation. InICML

    2024

  5. [5]

    Zhangqian Bi, Yao Wan, Zheng Wang, Hongyu Zhang, Batu Guan, Fangxin Lu, Zili Zhang, Yulei Sui, Hai Jin, and Xuanhua Shi. 2024. Iterative Refinement of Project-Level Code Context for Precise Code Generation with Compiler Feedback. InFindings of ACL

    2024

  6. [6]

    Matteo Biagiola, Jahrim Gabriele Cesario, Luca Di Grazia, George Zakhour, and Guido Salvaneschi. 2026. The Alignment Problem in Constrained Code Generation

    2026

  7. [7]

    Andrew Blinn, Xiang Li, June Hyung Kim, and Cyrus Omar. 2024. Statically Contextualizing Large Language Models with Typed Holes.Proc. ACM Program. Lang.OOPSLA2 (2024)

    2024

  8. [8]

    Pantazis Deligiannis, Akash Lal, Nikita Mehrotra, Rishi Poddar, and Aseem Rastogi. 2025. RustAssistant: Using LLMs to Fix Compilation Errors in Rust Code. InICSE

    2025

Show all 63 references
  1. [9]

    Shihan Dou, Yan Liu, Haoxiang Jia, Enyu Zhou, Limao Xiong, Junjie Shan, Caishuang Huang, Xiao Wang, Xiaoran Fan, Zhiheng Xi, Yuhao Zhou, Tao Ji, Rui Zheng, Qi Zhang, Tao Gui, and Xuanjing Huang. 2024. StepCoder: Improving Code Generation with Reinforcement Learning from Compil...

    2024

  2. [10]

    Yufeng Du, Minyang Tian, Srikanth Ronanki, Subendhu Rongali, Sravan Babu Bodapati, Aram Galstyan, Azton Wells, Roy Schwartz, Eliu A Huerta, and Hao Peng. 2025. Context Length Alone Hurts LLM Performance Despite Perfect Retrieval. InFindings of EMNLP

    2025

  3. [11]

    Jonás Fiala, Shachar Itzhaky, Peter Müller, Nadia Polikarpova, and Ilya Sergey. 2023. Leveraging Rust Types for Program Synthesis.Proc. ACM Program. Lang.PLDI (2023)

    2023

  4. [12]

    Emmanuel Anaya Gonzalez, Sairam Vaidya, Kanghee Park, Ruyi Ji, Taylor Berg-Kirkpatrick, and Loris D’Antoni. 2026. Constrained Sampling for Language Models Should Be Easy: An MCMC Perspective. InNeurIPS

    2026

  5. [13]

    Google DeepMind. 2026. Gemini 3.5 Flash Model Card. https://storage.googleapis.com/deepmind-media/Model- Cards/Gemini-3-5-Flash-Model-Card.pdf

    2026

  6. [14]

    Tihomir Gvero, Viktor Kuncak, Ivan Kuraj, and Ruzica Piskac. 2013. Complete completion using types and weights. In PLDI

    2013

  7. [15]

    Son Ho and Jonathan Protzenko. 2022. Aeneas: Rust verification by functional translation.Proc. ACM Program. Lang. ICFP (2022)

    2022

  8. [16]

    Pierce, and Philip Wadler

    Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. 2001. Featherweight Java: a minimal core calculus for Java and GJ.ACM Trans. Program. Lang. Syst.23, 3 (2001), 396–450

    2001

  9. [17]

    Juyong Jiang, Fan Wang, Jiasi Shen, Sungju Kim, and Sung Hun Kim. 2026. A Survey on Large Language Models for Code Generation.ACM Trans. Softw. Eng. Methodol.35, 2 (2026)

    2026

  10. [18]

    Gregory Morrisett, Dan Grossman, Michael W

    Trevor Jim, J. Gregory Morrisett, Dan Grossman, Michael W. Hicks, James Cheney, and Yanling Wang. 2002. Cyclone: A Safe Dialect of C. InUSENIX ATC

    2002

  11. [19]

    Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. 2018. RustBelt: securing the foundations of the rust programming language.Proc. ACM Program. Lang.POPL (2018)

    2018

  12. [20]

    Anirudh Khatry, Robert Zhang, Jia Pan, Ziteng Wang, Qiaochu Chen, Greg Durrett, and Isil Dillig. 2025. CRUST-Bench: A Comprehensive Benchmark for C-to-safe-Rust Transpilation. InCOLM

    2025

  13. [21]

    Shriram Krishnamurthi and Matthew Flatt. 2026. Type-Error Ablation and AI Coding Agents.arXiv Preprint abs/2606.01522 (2026)

    2026 arXiv

  14. [22]

    Lerner, Matthew Flower, Dan Grossman, and Craig Chambers

    Benjamin S. Lerner, Matthew Flower, Dan Grossman, and Craig Chambers. 2007. Searching for Type-Error Messages. InPLDI

    2007

  15. [23]

    MacIver, Li Du, Jason Eisner, Ryan Cotterell, Vikash Mansinghka, Timothy J

    Benjamin Lipkin, Benjamin LeBrun, Jacob Hoover Vigly, João Loula, David R. MacIver, Li Du, Jason Eisner, Ryan Cotterell, Vikash Mansinghka, Timothy J. O’Donnell, Alexander K. Lew, and Tim Vieira. 2025. Fast Controlled Generation from Language Models via Adaptive Weighted Rejec...

    2025

  16. [24]

    Liu, Kevin Lin, John Hewitt, Ashwin Paranjape, Michele Bevilacqua, Fabio Petroni, and Percy Liang

    Nelson F. Liu, Kevin Lin, John Hewitt, Ashwin Paranjape, Michele Bevilacqua, Fabio Petroni, and Percy Liang. 2024. Lost in the Middle: How Language Models Use Long Contexts.TACL12 (2024)

    2024

  17. [25]

    Lew, Tim Vieira, and Timothy J

    João Loula, Benjamin LeBrun, Li Du, Ben Lipkin, Clemente Pasti, Gabriel Grand, Tianyu Liu, Yahya Emara, Marjorie Freedman, Jason Eisner, Ryan Cotterell, Vikash Mansinghka, Alexander K. Lew, Tim Vieira, and Timothy J. O’Donnell

  18. [26]

    Guillaume Marceau, Kathi Fisler, and Shriram Krishnamurthi. 2011. Measuring the effectiveness of error messages designed for novice programmers. InSIGCSE

    2011

  19. [27]

    Nicholas D Matsakis and Felix S Klock. 2014. The rust language.ACM SIGAda Ada Letters34, 3 (2014)

    2014

  20. [28]

    Yusuke Matsushita, Takeshi Tsukada, and Naoki Kobayashi. 2021. RustHorn: CHC-based Verification for Rust Programs. ACM Trans. Program. Lang. Syst.4 (2021)

    2021

  21. [29]

    Daniel Melcer, Nathan Fulton, Sanjay Krishna Gouda, and Haifeng Qian. 2024. Constrained Decoding for Fill-in-the- Middle Code Language Models via Efficient Left and Right Quotienting of Context-Sensitive Grammars

    2024

  22. [30]

    Moonshot AI. 2026. Kimi-K2.7-Code. https://huggingface.co/moonshotai/Kimi-K2.7-Code

    2026

  23. [31]

    Niels Mündler, Jingxuan He, Hao Wang, Koushik Sen, Dawn Song, and Martin Vechev. 2025. Type-Constrained Code Generation with Language Models.Proc. ACM Program. Lang.PLDI (2025)

    2025

  24. [32]

    Andrew C. Myers. 1999. JFlow: Practical Mostly-Static Information Flow Control. InPOPL

    1999

  25. [33]

    Niels Mündler, Jasper Dekoninck, and Martin Vechev. 2026. Constrained Decoding of Diffusion LLMs with Context-Free Grammars. InICLR

    2026

  26. [34]

    Shaan Nagy, Timothy Zhou, Nadia Polikarpova, and Loris D’Antoni. 2026. ChopChop: A Programmable Framework for Semantically Constraining the Output of Language Models.Proc. ACM Program. Lang.POPL (2026)

    2026

  27. [35]

    Cyrus Omar, Ian Voysey, Ravi Chugh, and Matthew A. Hammer. 2019. Live functional programming with typed holes. Proc. ACM Program. Lang.POPL (2019)

    2019

  28. [36]

    Cyrus Omar, Ian Voysey, Michael Hilton, Jonathan Aldrich, and Matthew A. Hammer. 2017. Hazelnut: a bidirectionally typed structure editor calculus. InPOPL

    2017

  29. [37]

    OpenAI. 2026. GPT-5.3-Codex System Card. https://deploymentsafety.openai.com/gpt-5-3-codex

    2026

  30. [38]

    Peter-Michael Osera and Steve Zdancewic. 2015. Type-and-example-directed program synthesis. InPLDI

    2015

  31. [39]

    Kanghee Park, Jiayu Wang, Taylor Berg-Kirkpatrick, Nadia Polikarpova, and Loris D’Antoni. 2024. Grammar-Aligned Decoding. InNeurIPS

    2024

  32. [40]

    Pearce, and Fausto Spoto

    Etienne Payet, David J. Pearce, and Fausto Spoto. 2022. On the Termination of Borrow Checking in Featherweight Rust.NASA Formal Methods(2022)

    2022

  33. [41]

    David J. Pearce. 2021. A Lightweight Formalism for Reference Lifetimes and Borrowing in Rust.ACM Trans. Program. Lang. Syst.43, 1 (2021)

    2021

  34. [42]

    Hammond Pearce, Baleegh Ahmad, Benjamin Tan, Brendan Dolan-Gavitt, and Ramesh Karri. 2022. Asleep at the Keyboard? Assessing the Security of GitHub Copilot’s Code Contributions. InIEEE S&P

    2022

  35. [43]

    Gabriel Poesia, Alex Polozov, Vu Le, Ashish Tiwari, Gustavo Soares, Christopher Meek, and Sumit Gulwani. 2022. Synchromesh: Reliable Code Generation from Pre-trained Language Models. InICLR

    2022

  36. [44]

    Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama. 2016. Program synthesis from polymorphic refinement types. InPLDI

    2016

  37. [45]

    Henrijs Princis, Arindam Sharma, and Cristina David. 2026. TreeCoder: Systematic Exploration and Optimisation of Decoding and Constraints for LLM Code Generation.Proc. ACM Program. Lang.PLDI (2026)

    2026

  38. [46]

    Rust Developers. 2026. rust-lang/rust-analyzer. https://github.com/rust-lang/rust-analyzer

    2026

  39. [47]

    rust-lang. 2026. rust-lang/rust: Empowering everyone to build reliable and efficient software. https://github.com/rust- lang/rust

    2026

  40. [48]

    Seidel, Huma Sibghat, Kamalika Chaudhuri, Westley Weimer, and Ranjit Jhala

    Eric L. Seidel, Huma Sibghat, Kamalika Chaudhuri, Westley Weimer, and Ranjit Jhala. 2017. Learning to blame: localizing novice type errors with data-driven diagnosis.Proc. ACM Program. Lang.OOPSLA (2017)

    2017

  41. [49]

    Rico Sennrich, Barry Haddow, and Alexandra Birch. 2016. Neural Machine Translation of Rare Words with Subword Units. InACL

    2016

  42. [50]

    Zhi Rui Tam, Cheng-Kuang Wu, Yi-Lin Tsai, Chieh-Yen Lin, Hung yi Lee, and Yun-Nung Chen. 2024. Let Me Speak Freely? A Study on the Impact of Format Restrictions on Performance of Large Language Models

    2024

  43. [51]

    Qwen Team. 2026. Qwen3.5: Accelerating Productivity with Native Multimodal Agents. https://qwen.ai/blog?id= qwen3.5

    2026

  44. [52]

    Shubham Ugare, Rohan Gumaste, Tarun Suresh, Gagandeep Singh, and Sasa Misailovic. 2025. IterGen: Iterative Semantic-aware Structured LLM Generation with Backtracking. InICLR

    2025

  45. [53]

    Shubham Ugare, Tarun Suresh, Hangoo Kang, Sasa Misailovic, and Gagandeep Singh. 2025. SynCode: LLM Generation with Grammar Augmentation.TMLR(2025)

    2025

  46. [54]

    Mark Vero, Niels Mündler, Victor Chibotaru, Veselin Raychev, Maximilian Baader, Nikola Jovanovic, Jingxuan He, and Martin Vechev. 2025. BaxBench: Can LLMs Generate Correct and Secure Backends?. InICML

    2025

  47. [55]

    Mitchell Wand. 1986. Finding the Source of Type Errors. InPOPL

    1986

  48. [56]

    Xin Wang, Yasheng Wang, Yao Wan, Fei Mi, Yitong Li, Pingyi Zhou, Jin Liu, Hao Wu, Xin Jiang, and Qun Liu. 2022. Compilable Neural Code Generation with Compiler Feedback. InFindings of ACL

    2022

  49. [57]

    Matsakis, and Amal Ahmed

    Aaron Weiss, Daniel Patterson, Nicholas D. Matsakis, and Amal Ahmed. 2019. Oxide: The Essence of Rust.arXiv Preprintabs/1903.00982 (2019). 1:30 Niels Mündler-Sasahara, Hristo Venev, Dawn Song, Martin Vechev, and Jingxuan He

    2019 arXiv

  50. [58]

    Chunqiu Steven Xia, Yinlin Deng, Soren Dunn, and Lingming Zhang. 2025. Demystifying LLM-Based Software Engineering Agents.Proc. ACM Softw. Eng.FSE (2025)

    2025

  51. [59]

    Jiahong Xiang, Wenxiao He, Xihua Wang, Hongliang Tian, and Yuqun Zhang. 2026. Evaluating and Improving Automated Repository-Level Rust Issue Resolution with LLM-based Agents. InICSE

    2026

  52. [60]

    Z.ai. 2026. GLM-5.2: Built for Long-Horizon Tasks. https://z.ai/blog/glm-5.2 Generative Compilation: On-the-Fly Compiler Feedback as AI Generates Code 1:31 A Experimental Details A.1 Construction ofUpdatedAPI For theUpdatedAPIdataset, we construct a benchmark that requires LLM...

    2026

  53. [62]

    Use this format for each regenerated file: {path/to/file.rs} ```rust // complete replacement Rust file ```

    Regenerate complete Rust files that should replace files from the current project state. Use this format for each regenerated file: {path/to/file.rs} ```rust // complete replacement Rust file ```

  54. [63]

    Use this exact patch format: *** Begin Patch *** Update File: path/to/file.rs @@ -old line +new line *** End Patch Omitted files stay fixed exactly as currently generated

    Return one or more patches that edit the previous output. Use this exact patch format: *** Begin Patch *** Update File: path/to/file.rs @@ -old line +new line *** End Patch Omitted files stay fixed exactly as currently generated. Fig. 18. Feedback message used byPost Compilati...

  55. [2025]

    InThe Thirteenth International Conference on Learning Representations

    Syntactic and Semantic Control of Large Language Models via Sequential Monte Carlo. InThe Thirteenth International Conference on Learning Representations. Generative Compilation: On-the-Fly Compiler Feedback as AI Generates Code 1:29

Pith tools

Reviewed August 2, 2026 · model on record in the stance chip above.