'Generative Compilation' Feeds Rust Errors Into LLM Decoding

When an AI writes Rust, the compiler usually only weighs in once the model has finished. A new arXiv paper from a team including Dawn Song and Martin Vechev argues that is the wrong order of operations. By the time an error surfaces, the model has already built more code on top of the mistake, and any post-hoc fix has to unwind the cascade.

The proposal is called generative compilation. The trick is a component the authors call a 'sealor,' described in the paper as 'a lightweight, mostly syntax-guided transformation that converts partial programs into complete ones that standard compilers can diagnose.' The point is not to compile the final program, it is to compile the fragment produced so far, catch errors close to their source, and feed that back into decoding. The design goal is that 'possible-to-complete partial programs are never rejected,' while still preserving enough context to spot genuine dead ends.

Rust is the natural first target. Languages with 'rich static semantics,' as the abstract puts it, are exactly where LLM output tends to fail late and expensively, and their strictness is what makes generation harder in the first place. The authors say they built the sealor on a 'Rust-like calculus' and mechanized the correctness proof in Lean, then extended it to what they call 'the first partial-program checker for real Rust.' That is a real engineering claim, not just a benchmark stunt.

The honest caveat is what the abstract does not give you. There are no headline percentage improvements, no named models on a leaderboard, no reproducible dataset the community can hammer at yet. The claim is qualitative, that generative compilation 'reduces non-compiling outputs and improves functional correctness' relative to standard post-generation feedback across 'frontier black-box and open-weight models.' Take the specifics as reported, not settled, and remember the Lean proof covers a calculus, not the messy corners of real Rust the production checker has to survive.

The downstream question is who benefits first. Any team running expensive frontier models against strongly typed codebases pays a token bill every time the model dead-ends. If a partial-program checker can catch that early enough to redirect decoding, the economics of using premium models on statically typed code start to look different, and the same idea points at Haskell, OCaml, and other strict languages next.