Sam Gleeson

Recent Writing

• Compiling Down to Physics: The Tower of Interpreters, All the Way DownMay 27, 2026

  If a compiler optimization is just runtime work you proved you don't have to do, why stop at machine code? Follow the thesis through the instruction set, the gates, the transistors, and off the digital cliff into analog and physics, and 'optimize the program' turns into 'find a physical system whose natural evolution is the program — and prove it.' This is the tower of interpreters, the verified spine that reaches down it, and the thermodynamic floor where it bottoms out.

• Running an EVM Inside a Proof AssistantMay 27, 2026

  Most EVMs you trust because they pass tests. This one you trust because the interpreter and its correctness proof are the same artifact, checked by a kernel you can't lie to. It executes real post-Cancun bytecode — decoder, stack machine, gas meter, fixture harness — and the same evaluator that runs your bytecode is the one a once-proved soundness theorem reasons about. Here's how that's possible, and why a single parametric `run` is the whole trick.

• Rented Power, Owned Trust: The Commercial Case for Certified Hyper-OptimizationMay 27, 2026

  If you can prove that fast code means what the original meant, you decouple optimization power from optimization trust — and you turn every competitor's optimizer, every frontier LLM, into your improvement. This post takes the thesis from 'Prove More, Run Less' and asks the next question: where does that capability actually pay, who buys it, and what's the single cheap experiment that decides whether the whole thing is real?

• Prove More, Run Less: When a Sound Analysis Becomes an Optimizing CompilerMay 26, 2026

  An abstract interpreter is a proof machine — every sound invariant it computes constrains what the program can possibly do at runtime. Push that far enough and the analysis stops describing the program and starts compiling it. This is the precise sense in which 'the more you prove, the less you run,' why it is almost the same thing as 'compiling by proving,' and how a refinement relation you already have becomes a certifying optimizer for free.

• One Substrate, Many Instruments: A General Framework for Program AnalysisMay 24, 2026

  Two tools is not a framework — it's two tools. What turns interpreters, abstract interpreters, symbolic executors, model checkers, type systems and provers into one bench is a shared substrate plus a six-slot instrument interface and one linking theorem per tool.