{"id":"b7846ceb-97e7-412c-9b50-62ea60b27d3c","arxiv_id":"2607.13921","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":3,"one_line_summary":"Turning compilers into prefix checkers by sealing partial programs enables early error feedback during AI code generation, reducing compilation errors and improving functional correctness.","lead":"This paper introduces a method for getting compiler feedback on partially written code while an AI is still generating it, before the program is finished. It works by 'sealing' incomplete code into compilable programs, allowing the Rust compiler to check it early, which reduces errors and improves correctness in AI-written Rust.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Real-Rust sealor completeness is unverified: §6.2 gives only informal per-feature arguments, so a single valid-prefix rejection (e.g., holeval() in an as-yet-unconstrained context) could break generative compilation; Table 1 does not test this property.","rationale":"The reader's weakest assumption already identifies the unproven real-Rust sealor completeness and the idealization of rustc as an exact compiler. My stress pass converges on the same point as the most load-bearing concern, because the entire value proposition of generative compilation depends on never rejecting a completable prefix: a false rejection injects a spurious diagnostic into the model's prompt and consumes a restart, directly affecting both compiler-error rate and functional correctness. The FR result, while mechanized in Lean, is limited to Featherweight Rust and cannot rescue the real-Rust implementation; §6.2 is explicit that the Rust rules are informal. I also credit the paper for the machine-checked FR development and for a fair end-to-end comparison that includes a fixed total feedback budget. The concern is therefore not that the empirical improvement is fabricated, but that its mechanism is not verified: the improvement could be robust even with an incomplete S_RS, or it could be fragile and task-specific. A direct prefix-invariant test would settle this by checking the exact property that Theorem 3.2 needs. Since the reader already marked the paper CONDITIONAL, my analysis does not move the verdict; it sharpens the condition by proposing a concrete, executable check.","tokens_in":33853,"tokens_out":12302,"duration_ms":138227,"concrete_test":"Run a prefix-invariant test: take a corpus of valid Rust programs (the authors' own task solutions, rustc's test suite, or a set of crates), enumerate token-level prefixes of each program, apply S_RS to every prefix, and invoke rustc on the sealed result. If any prefix of a valid program is rejected by rustc, S_RS is not globally complete; record the first such counterexample and check whether the failing case is due to holeval()/E0282 or another rule. If no counterexample is found across a sufficiently large and diverse corpus, the practical completeness concern is substantially weakened. If counterexamples are found, re-analyze Table 1 to determine how often the affected prefix pattern occurs and whether the reported error-rate/correctness gains persist when those spurious rejections are removed.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central practical claim is that generating with on-the-fly compiler feedback reduces errors and improves correctness. The mechanism that makes the feedback trustworthy is the real-Rust sealor's global completeness: a prefix that admits a valid completion must never be rejected, because rejection triggers a costly restart with potentially spurious diagnostics. The FR sealor has this property mechanized in Lean, but the paper explicitly does not extend the proof to Rust. §6.2 states: 'we give informal, per-feature arguments for typing behavior, completeness, and soundness, rather than the formal, mechanized treatment we gave for the whole FR.' Theorem 3.2 then requires an exact compiler C and a complete sealor S. For rustc, exactness is an idealization; for S_RS, completeness is not demonstrated at all. There is a concrete mechanism to worry about: the expression sealor appends holeval(), a generic call whose type parameter T is inferred from context. When the surrounding code has not yet constrained T—for example a partial closure body or a partial block used as an expression whose expected type is determined only by later code—rustc may emit E0282 ('type annotations needed'), rejecting a prefix that could be completed to a valid program. The paper suppresses E0282 only inside partial function bodies, not necessarily in all expression contexts where holeval() is inserted. If such a rejection exists, S_RS is not globally complete, and GC can send the model spurious feedback. The empirical evaluation measures end-to-end outcomes on 14 configurations but never checks the completeness invariant directly; favorable numbers could still hold even if S_RS rejects some valid prefixes, so the result would not generalize to the claimed completeness guarantee.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":34224,"tokens_out":6822,"duration_ms":80175,"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":[{"comment":"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","section":"§6.2, §6.1"},{"comment":"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.","section":"§5.3, Theorem 5.3"},{"comment":"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.'","section":"§5.4, Lemma 5.4 and Theorem 5.5"},{"comment":"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.","section":"§8"}],"minor_comments":[{"comment":"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.","section":"§6.1"},{"comment":"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.","section":"§6.2"},{"comment":"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.","section":"§7.1, Table 1"},{"comment":"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.","section":"§7.3"}],"recommendation":"major_revision","confidential_remarks":"The FR formalization and the general sealor framework are credible and could be published on their own. The main risk is the real-Rust extension: the paper's strongest practical claims depend on an unverified completeness guarantee for S_RS, and the diagnostics quality—the method's raison d'être—is outside the formal results. I would ask the authors to either close these gaps or substantially reframe the claims as an empirical system with a formal core for a core calculus. The paper is worth a major revision rather than rejection."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Generative compilation is a real contribution. The idea—sealing partial programs so an off-the-shelf compiler can give feedback mid-generation—is new and well-motivated. The FR formalization with Lean mechanization is substantial, and the Rust implementation is a serious engineering effort. The empirical evaluation is broad: seven models, two repo-level tasks, and the comparison against post-generation feedback mostly favors GC. The analysis showing errors are reported near their source and with fewer diagnostics is useful.\n\nThe soft spots are real but not fatal. The completeness and soundness guarantees are proven only for FR. For real Rust, the paper explicitly gives informal per-feature arguments. The stress-test worry about holeval() in contexts where the type parameter is underconstrained is plausible: E0282 suppression is scoped to function bodies, and there are expression positions (e.g., partial closure bodies with no signature) where rustc could reject a completable prefix. This is a genuine gap in the completeness claim, but the empirical results suggest the practical impact is limited. The paper would be stronger if it either extended the suppression or reported how often such false rejections occur in the replay analysis.\n\nThe selective soundness result at statement boundaries is nearly tautological—it holds because SFR(b) outputs the same term that realizes it—and the diagnostics-quality question is explicitly left out of the formalization. The empirical tables also lack confidence intervals, though the paired difference test at 5% provides some support.\n\nOverall, the central claim holds: on-the-fly feedback helps. The paper deserves a serious referee. It's an original piece of work with reproducible artifacts (Lean proofs, code, data) and a clear limitation section. I'd send it to review, asking the authors to either tighten the Rust completeness argument or reframe the claims accordingly.","headline":"A solid, original paper with real results; the Rust sealor's informal completeness is the main gap, but the empirical case holds.","tokens_in":34739,"tokens_out":2566,"would_cite":true,"duration_ms":25361,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"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","keywords":["generative compilation","sealor","partial programs","compiler feedback","Rust","LLM code generation","prefix checking","constrained decoding"],"falsifier":"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.","tokens_in":33747,"feed_emoji":"🦀","tokens_out":6018,"duration_ms":61841,"temperature":0.7,"pith_summary":"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.","feed_headline":"On-the-fly compiler feedback cuts AI Rust errors by a third","feed_subtitle":"A lightweight pass fills in half-written code so standard compilers can flag dead ends while the model is still writing.","key_machinery":"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.","core_discovery":"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","pith_inferences":["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."],"forward_implications":["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."],"fun_headline_variants":["Compiler feedback during codegen cuts Rust errors in AI code","Sealor lets compilers spot dead ends as AI writes code","On-the-fly compiler feedback improves AI-generated Rust correctness","Partial-program checker reduces non-compiling AI Rust outputs","New sealor makes standard compilers work on incomplete AI code"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Compiler feedback during codegen cuts Rust errors in AI code","Sealor lets compilers spot dead ends as AI writes code","On-the-fly compiler feedback improves AI-generated Rust correctness","Partial-program checker reduces non-compiling AI Rust outputs","New sealor makes standard compilers work on incomplete AI code"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000724,"raw_usage":{"total_tokens":3115,"prompt_tokens":807,"completion_tokens":2308,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":551,"completion_tokens_details":{"reasoning_tokens":2225}},"tokens_in":551,"tokens_out":2308,"duration_ms":18644,"temperature":1.0,"reasoning_tokens":2225,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-02T03:19:03.575152+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[],"review_version":1}