Ship Your Interpreter

Handwritten language rules can disagree with the interpreter people actually run; compile that interpreter to a modeled processor and prove its behavior matches the rules for every program.

Read the paper ↗

The short version

What it is

Interpreter-to-semantics refinement Write precise rules for a language, then check that they predict exactly what its existing interpreter does.
Compiled interpreter as the reference Compile the interpreter to a processor with a formal machine model, so the comparison reaches the executable rather than stopping at a sketch of it.
Proof obligations as feedback When a rule cannot be proved to match the interpreter, the failed obligation can point to a behavior the rule missed.

Why it matters

A language’s rules become a foundation for other proofs. Checking them against the interpreter helps catch subtle mismatches that tests can miss, while making clear that agreement with an implementation is not the same as proving the implementation matches an ideal design.

Before we dive in, here’s the basic idea: write down what a language means, then check those rules against the interpreter people actually run. The twist is that the interpreter itself gets compiled to a processor with a formal model, so the comparison reaches the executable rather than stopping at a tidy sketch of its behavior.

Specification: Before you can prove a program correct, you need rules that say what its loops, functions, and operations do. Many languages leave those details in informal documentation and implementation choices. The canonical example here is an extended WHILE language: its interpreter defines practical behavior, while the formal rules are meant to predict the same behavior. Once that clicks, the general problem is clear: a rule set is useful only if it describes the language people run.
Trust: Tests tell you what happened on examples someone selected; they don’t establish that the rules are right for every program. One concrete example is string concatenation with a function value: the interpreter truncates the displayed function name at 63 bytes, a small implementation detail that a hand-written rule can easily omit. That detail is observable, so a semantics that misses it can support proofs about behavior users never get. The limit of the example is that it illustrates one mismatch, not a complete recipe for finding all of them. So how do we compare rules with the real interpreter rather than a handful of examples?

The key move is to compile the existing interpreter to RISC-V, whose instruction behavior has a formal model, and then prove the language rules agree with that compiled program. In everyday terms, it is like checking a map against the route a delivery driver actually takes, not against a few trips you happened to watch; the analogy stops short because the proof covers formal execution behavior, not every judgment about what the route ought to be.

The comparison asks whether the rules predict the same printed result as the binary. More precisely, the semantic output relation and successful machine output relation are equivalent: $\mathrm{BigStep}(p,o) \iff \mathrm{Halts}(c,o,0)$ . In words, the semantics predicts an output exactly when the loaded machine run prints it and exits successfully. There is also a divergence condition: if the machine runs forever, the semantics must not claim a terminating output. Together, these obligations cover both directions of successful behavior and rule out a mismatch hidden behind nontermination.

So this is not just testing the interpreter on representative programs. The proof obligation applies to every program represented by the theorem, provided the machine state really is loaded to run that program. Establishing that starting condition matters; otherwise the theorem could say something true about a machine state nobody can reach. What happens when the semantic rule and the executable disagree?

The useful answer is that the proof gets stuck. If the semantics allows an output the binary does not produce, one direction fails; if the interpreter produces an output the semantics cannot derive, the other direction fails. In the function-string example, the rule had to include the 63-byte truncation before the concatenation case could be proved. The same feedback led to rules accounting for wrapped integer arithmetic, a for initializer’s treatment of abrupt status, and built-ins rendering differently in printing and concatenation.

I like this because it turns implementation quirks into explicit questions instead of burying them in test coverage. But the target is agreement, not approval: the method can validate that the semantics matches the interpreter, including behavior you might consider odd. And it relies on the loaded-state connection being established. How far can you trust rules once that bridge is in place? Other work in the project handles heap-dependent ownership specifications needed for allocation; the core point here is the end-to-end match between language rules and executable behavior.

Read the deep dive

Why People Wanted It

A proof about a program is only as trustworthy as the description of what that program means. But many languages have no formal semantics: their practical meaning lives in an interpreter or compiler, while a new mathematical account must be written by hand. The problem is not merely whether that account looks plausible. It is whether its rules match the behavior users get from the implementation.

Tests help, but they only examine programs someone thought to try. A semantics can pass a test suite and still miss an observable detail. The real question is: can you check a language’s rules against the interpreter itself, rather than treating the rules as an unquestioned starting point?

The Core Move

Compile the existing interpreter to a processor with a formal machine model, then prove that the language semantics and the compiled interpreter agree on every program.

For a program $p$ and output $o$ , the terminating part of the claim is $\mathrm{BigStep}(p,o) \iff \mathrm{Halts}(c,o,0)$ , where $c$ is a loaded machine state running the interpreter on $p$ . In words: the semantics predicts an output exactly when the binary halts successfully after printing that output.

Quiz

What does the refinement theorem establish about a source program and the compiled interpreter?

The theorem proves that every machine configuration is a valid interpreter run.

The semantics and the binary agree on successful outputs under a loaded-state condition, with a separate condition covering divergence.

The binary is guaranteed to implement the language’s intended design, even if the interpreter behaves differently.

The semantics only needs to predict outputs for a sample of tested programs.

Why Interpreter Refinement Needs Both Directions

Now the version for readers who want more of the machinery: refinement is not just checking that semantic predictions are possible; it rules out both missing behavior and invented behavior. The loaded-state condition connects a source program to a machine configuration that is about to run the interpreter binary on that program.

The equivalence $\mathrm{BigStep}(p,o) \iff \mathrm{Halts}(c,o,0)$ has two obligations. The left-to-right direction says every output derived by the semantics is actually printed by a successful binary run. The right-to-left direction says every successful output from the binary is derivable in the semantics. If the semantics is too permissive, the first direction fails; if it is too strict, the second does.

Termination alone leaves a gap: a semantic rule might predict no output while the interpreter runs forever. So the theorem also states $\mathrm{Diverges}(c) \Rightarrow \neg\exists o\,\mathrm{BigStep}(p,o)$ . In words, a machine execution that diverges cannot coexist with a terminating semantic derivation. Together, these claims connect the semantics to both successful termination and divergence, rather than only comparing outputs on runs that happen to halt.

Why the Proof Reaches the Compiled Machine Code

Here is the part that gets technical: the machine-level theorem makes the interpreter’s implementation, not a simplified model of it, the endpoint of the argument. The interpreter is compiled to RISC-V, whose instruction behavior has a formal model translated into Lean. The executable, C compiler output, C library, and allocator are inside the theorem’s scope.

That does not mean a reader has to inspect every instruction to understand the claim. The key interface is the theorem statement: a Loaded machine configuration connects the source program to the binary’s starting state, and the conclusions compare semantic outputs with what the machine prints. The proof discharges the low-level execution details underneath that interface. This is an end-to-end refinement claim, conditional on the loaded-state hypothesis—not a claim that every arbitrary machine state represents a valid interpreter run.

The condition matters: a theorem about an unreachable or impossible starting state could be vacuous. What makes the interface useful is establishing that Loaded actually holds for concrete programs. The construction of those states and their validation connect the abstract precondition back to executions of the executable. How do you know what the failed obligations are telling you about the language rules?

Why Failed Obligations Can Correct the Semantics

Now one level deeper: a failed proof obligation can expose a mismatch at the exact boundary where a semantic rule meets observable interpreter behavior. The proof does not magically choose the right rule; it forces the proposed rule to account for the implementation’s behavior in both directions.

For example, function values concatenated with strings are rendered with a length limit: the semantics had to account for taking at most 63 bytes of the function’s displayed name. A concatenation proof could not close for longer names until the rule reflected that behavior. Other corrections included 64-bit wrapping integer arithmetic, the for loop initializer’s handling of abrupt status, and distinct rendering of built-ins in printing versus concatenation.

The same pattern applies to statements about library routines: if a claimed behavior of a C library function disagrees with its machine code, that lemma’s obligation also gets stuck. The practical loop is therefore precise: propose rules, prove agreement, and revise the rule exposed by a mismatch. It validates agreement with the interpreter’s actual behavior; whether that behavior is desirable is a separate question.

Minimal Causal Code

This is the shape of the refinement check, not a fast evaluator. The state and the proof obligations stay visible; a real development proves these relations in Lean over the loaded machine execution.

# p: source program; c: loaded machine state running the interpreter on p
for p in programs:
    c = load_interpreter_state(p)

    for out in semantic_outputs(p):
        assert machine_halts_and_prints(c, out, exit_code=0)

    for out in machine_successful_outputs(c):
        assert semantics_derives(p, out)

    if machine_diverges(c):
        assert not semantics_has_terminating_output(p)

What You Gain, and What You Lose

You gain a way to validate readable language rules against the interpreter people actually run, including observable quirks that ordinary tests may miss. Once a semantics is connected to the binary, later proofs stated against those rules can be composed with the refinement result.

You do not get a proof that the interpreter implements the language you wish it had; you get agreement with the interpreter’s behavior. Nor is the proof free of assumptions: the theorem depends on the loaded-state condition, and establishing that condition is part of making the result meaningful. The low-level proof also carries substantial complexity in the compiled code and runtime. This module focuses on the refinement argument, not the separate heap-ownership machinery used to make memory reasoning tractable.

Core Takeaway

Treat the interpreter as the behavior to match, and make every language rule earn its place in a proof against the compiled binary.