Ship Your Interpreter

www.basis.ai 5 pages Read the paper

The short version

The problem: To prove software safe, you first need an exact description of what its programming language means. Writing that description is difficult, and tests can miss small but important differences between the rules and the interpreter people actually run.
The idea: The paper treats the real interpreter as the reference point: it compiles the interpreter to a processor model whose behavior is formally specified, then proves that the language rules predict the same results. It is like checking a written instruction manual against a machine that follows the original instructions, for every possible program—not just a set of test cases.
What it got: For a small programming language, the team proved this agreement and used the rules to build verified programming tools, including a compiler. On the programs tested, that compiler executed between 2.7 and 8.2 times fewer instructions than the interpreter.

Modules from this paper

Heap-Dependent Ownership for malloc

A fixed write footprint cannot describe how malloc’s writes vary with allocation state; separation logic makes the allocator’s owned memory depend on which blocks are live.

separation-logicmemory-safetyformal-verificationinterpreters

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.

formal-semanticsprogram-verificationinterpretersrefinement