One Behavior, Many Views: Interpreters, Compilers and Provers as Lenses on One Object

Here is a confusion worth dissolving. You can hand the same program to five different tools — an interpreter, a compiler, an abstract interpreter, a symbolic executor, a theorem prover — and get five different answers. One says r = 6. One says r is positive. One says the compiled stack code preserves the result. One proves r = n! for all inputs. Are they disagreeing? Is one of them right and the rest approximations of it?

No. They are all telling the truth, and none of them contradict each other. The reason is the whole point.

One object

There is a single underlying thing: a program's behavior. Extensionally it's a partial function Program × Input ⇀ Output — equivalently a relation, or a set of execution traces, or (with effects) an interaction tree. Everything those five tools produce is a view of this one object. They are coordinate systems on a single space.

Each tool reads a description of the behavior — a semantics — plus its own extra inputs, and reports something true. The differences between them aren't disagreements about what the program does. They're differences in what question each tool is built to answer and how much it deliberately throws away to answer it cheaply and decidably.

Different precision, not different truth

The views sit at different rungs of a precision lattice. "Exactly 6" and "positive" and "even" and "in [1, ∞]" are all true of the same value — coarser answers contain the truth rather than conflicting with it. A sound abstract interpreter is never wrong; it is, by design, only vague. That's what soundness means: the Galois obligation α ∘ F ∘ γ ⊑ F♯ certifies that the abstract transfer never under-approximates the concrete one. The only kind of answer that can actually lie is an unsound one.

Non-contradiction is earned, not free

Here is the load-bearing claim. If two tools literally share the same semantics generator, their agreement is automatic — they read the same thing. The instant they read different descriptions (KEVM's rewrite rules vs. the execution-layer reference spec; small-step vs. big-step; source vs. compiled target), agreement becomes a theorem you owe:

• small-step ≡ big-step — equivalence
• operational ≡ denotational — adequacy / full abstraction
• concrete ⊒ abstract — Galois soundness
• source ⊒ target — simulation / refinement (the CompCert theorem)
• model ≡ reference — conformance / differential testing

Each of these certifies that two descriptions denote the same object, and each names the failure mode it rules out. The failure mode they all exist to prevent is drift: two views of "the same" behavior that have quietly diverged. Skip the linking theorem and drift is exactly what you get.

This is why a framework like K is such a strong bet: write the semantics once as rewrite rules and the parser, concrete interpreter, symbolic executor and deductive verifier are all derived from that one definition — correct-by-construction, no per-tool re-description, no gap to drift into. The one thing that does not fall out for free is the sound abstract interpreter, because it needs structure (a Galois connection, a best transformer, join and widening, a fixpoint) that K doesn't synthesize. Whether that missing structure can be derived cheaply enough to beat hand-writing it is a live research question.

---

I built this up as a visual, interactive explainer: a single factorial computation refracted through six lenses you can click, a precision lattice you can walk node by node, the five semantic styles for one while loop side by side, and an expandable list of the linking theorems with the drift each one forbids.

→ Open the interactive explainer

The flashcards below are the TL;DR — the conceptual moves worth leaving the page with.