Interpreters, compilers, and compiler generators are not different kinds of artifact. They are points on one continuum, connected by specialization. That result is more than fifty years old, well understood, and it's the structural argument behind this toolchain.
Partial evaluation takes a program and some of its inputs, and produces a new program specialized to those inputs. Yoshihiko Futamura observed in 1971 that applying this idea to an interpreter produces a sequence of three constructions, now known as the Futamura projections.
| Projection | Specialize | Yields |
|---|---|---|
| First | Specialize an interpreter to a program | An executableThe program stops being data the interpreter reads and becomes code that runs. |
| Second | Specialize the specializer to an interpreter | A compilerA compiler is derived rather than written. This is how PyPy generates its interpreters. |
| Third | Specialize the specializer to itself | A compiler generatorThe construction closes on itself, which is the result that makes the sequence more than a trick. |
The projections are not a historical footnote. The second projection is the mechanism behind PyPy, which generates interpreters faster than the reference implementation, and behind the partial evaluation approach used for high performance language interpreters on the JVM. Today's just in time compilers use variations of the first projection, specializing an interpreter at runtime against observed behavior.
Specialize to the fabric, get a circuit
Every projection so far produces software. Specializing an interpreter to a program yields an executable; specializing the specializer yields a compiler. Each output is another program.
The step this toolchain takes is to specialize against a spatial dataflow fabric rather than against an instruction set. The output is not a program that runs on hardware. It's an arrangement of hardware. The same specification that the interpreter executes is what the tiles are placed from, which is why the obligation on each transition is stateable at all.
That's what the fourth rung is for, and it isn't speed. Getting a model running on new silicon is largely a solved problem already. What no amount of testing settles is whether the arrangement computes what the reference computes, and one specification descending every level is what makes that provable rather than sampled. The limit this is aimed at is the Verification Wall.
Source
LOGOS, the executable specification
Proof obligation dischargedsemantics preserved
Interpreter
Reference semantics, software
Proof obligation dischargedsemantics preserved
Register VM
Sequential execution model
Proof obligation dischargedsemantics preserved
Dataflow tiles
Spatial placement, physical fabric
The tip lands on the chip.
ProvenZero counterexamples
Every lowering discharges its proof obligation in our proof kernel, and the 8x8 run of the int8 matmul primitive matches an independent reference oracle, checksum 510,720. The kernel behind that proof finishes families Z3 and Kissat do not.
LOGOS is a programming language we developed, with its source published under Business Source License 1.1 and converting to MIT on 2029-12-24. It reads as structured English, and it's the single executable specification that appears at every level of the ladder above: the software interpreter runs it, the register virtual machine runs it, and the dataflow tiles are placed from it.
That single representation is what makes the approach work. When the specification, the reference implementation, and the thing being compiled are three separate artifacts, agreement between them is something you test for. When they are one artifact viewed at different levels, agreement is something you prove.
We are now using LOGOS to express hardware specifications, so that a design is described logically rather than drawn, and the placement is searched for rather than hand tuned.
LOGOS source is published and independently inspectable at github.com/Brahmastra-Labs/logicaffeine, under Business Source License 1.1, converting to MIT on 2029-12-24, with documentation and the studio at logicaffeine.com. One specification is used at every level: the interpreter, the register virtual machine and the dataflow tiles all derive from the same source, and placements are optimal against a named cost model and constraint set, so the claim is checkable.
The language, its syntax guide, and an interactive studio are published separately.
Source: LOGOS source, github.com/Brahmastra-Labs/logicaffeine(opens in a new tab)
Source: LOGOS documentation and studio, logicaffeine.com(opens in a new tab)
The standard treatment of partial evaluation, covering the projections and the machinery behind them, is Jones, Gomard, and Sestoft, Partial Evaluation and Automatic Program Generation, Prentice Hall, 1993. Futamura returned to the original result and reflected on it in 1999.
How is the obligation on each transition actually discharged?