In the workshop
Turns written code into a running program — and checks its own maths on the way.
Rust workspaceZ3-verified passes
Cast being recorded
A compiler workspace: AST to typed IR with dialects, Cranelift codegen, and Z3 verification of its own transformations.
People write programs in words that humans can read. Computers only understand numbers. A compiler is the translator in between.
Translators can make mistakes — and a mistake here breaks every program it touches. So this one does something unusual: after each step of the translation, it does a little bit of maths to prove the meaning didn’t change.
AST → typed IR lowering with dialects, Cranelift backend for native codegen, diagnostic codes, and Z3 SMT verification applied to transformation passes. The verification is the interesting part: optimisation passes are exactly where compilers silently change program meaning.
Rust workspace Cranelift codegen Z3 pass verification
No performance claims here, and none coming until there is a benchmark harness that runs in CI against a real machine. The 90-second recording planned for the Arcade shows it catching one real miscompilation — a claim that can be watched rather than believed.
Most hobby compilers stop at “it produces a binary”. Verifying passes with an SMT solver is graduate-level territory, and it is the difference between a toy and a thing worth reading.
| Language | Rust |
|---|---|
| Backend | Cranelift |
| Verification | Z3 SMT over transformation passes |
| Status | Working; benchmark harness not yet built |
Cast being recorded