One Behavior, Many Views An interpreter, a compiler, an abstract interpreter, a symbolic executor, and a theorem prover walk into a program. They each say something true. None of them contradict each other. Here is why — visually, with one worked example you can poke at.

00The thesis, in four lines

This is the conceptual companion to the repo's three partition surveys and the while-derivation-study. Where those ask "which languages/formats land where," this one asks the deeper question underneath: in what sense are all these tools talking about the same thing at all?

01The one object — four ways to write down the same behavior

Our worked example, threaded through the whole page. A tiny imperative (WHILE) program that computes a factorial:

The behavior of this program is a single mathematical object. We can write it down in different notations, but they all pin down the same thing — the same input/output pairs, the same trace. Switch between four equivalent descriptions:

02Six lenses on one computation — click a tool

Each tool below reads (a description of) that behavior and reports a view. The center chip is the ground truth. Watch the relation symbol change: = exact, ⊑ refines, α over-approximates, ⊢ proves a property about. None of these answers is wrong. They live at different precisions.

Every lens is reading the same semantics of WHILE. The difference is not the program and not the meaning — it is what question each tool is built to answer and how much it deliberately throws away to answer it decidably/cheaply.

03The precision lattice — coarser views are still true

The abstract-interpretation lens isn't a single thing — it's a whole tower. Pick how much detail to keep, and you get a different (still sound) answer for r after the loop. Lower = more precise; higher = cheaper & more decidable. Each rung is connected to the concrete by a Galois connection (α, γ): abstract up with α, concretize down with γ.

This tower is exactly what the pilot derives: the EVM Sign domain over 256-bit words, with the per-rule obligation α ∘ F ∘ γ ⊑ F♯ certifying that the abstract transfer never under-approximates the concrete one.

04Semantic styles — the same meaning, written five ways

Before any tool runs, someone has to describe the behavior. There are several house styles for doing so. They are interchangeable presentations of the same meaning — and the equivalences between them (§07) are theorems. Here is the WHILE while-loop construct in each:

05Computational substrates & their natural styles

Underneath the semantic styles sit a few models of computation. They're all Turing-equivalent as machines — but each makes a different style cheap, which is why specific tools cluster on specific substrates. The substrate is the medium; the style is what you paint with it.

06What's actually shared — the three-and-a-half layer factoring

If all these tools view one object, what exactly do they have in common, and what is per-tool? Factoring a "semantics" reveals the shared spine. Toggle a layer to see who owns it:

Named instances of this "base + interpretation" pattern: skeletal semantics (skeleton + semantic functions), tagless-final / monadic interpreters, and this repo's Rule_ir + Domain functor — one rule IR, instantiate the domain to get the concrete interpreter or the Sign analyzer.

07Linking theorems — the receipts that forbid contradiction

This is the load-bearing section. "They won't contradict each other" is true because of these theorems, not in spite of missing them. Each one certifies that two descriptions of behavior denote the same object — and each names the failure mode (drift) it rules out. Expand each:

08"Theorem prover" is four different things

A recurring confusion from the dialogue: a theorem prover is not a Turing machine of a special kind — it's a program that manipulates proofs, and the family splits along two axes (who drives, and what's trusted). Curry–Howard is why this is even coherent: a proof is a program, a proposition is a type, so "checking a proof" and "type-checking a program" are the same operation.

09K framework — write the semantics once, get the lenses for free

This is the payoff and the reason the repo exists. K's bet is the synthesis made operational: define ①b once as rewrite rules, and the tools below are derived from that one definition — correct-by-construction, no per-tool re-description, no drift. The meta-theory chain rewriting logic → matching logic → reachability logic is what makes each derivation a theorem.

10Watch / listen — the same ideas from the people who built them

If you watch two: Roșu for the framing, Cousot (J.P. Morgan) for the soundness half. Together they cover both halves of "all sound views of one behavior, related by α/γ and linking theorems."