Much Still to Do in Compiler Verification (A Perspective from the CakeML Project)
summary
End-to-end verified compiler for an ML-like language (the CakeML stack) compiles functions in the proof assistant logic down to concrete machine bytes and successfully bootstraps the compiler inside that logic, produces a JIT/REPL that generates and executes code, and ships a verified unsat proof checker used in a competition. It integrates a verified garbage collector, proves a cost-space semantics to rule out out-of-memory failures, shows performance comparable to OCaml/SML/NJ, and highlights remaining gaps: awkward cost reasoning, poor interoperability and modular reuse, and open work on verified separate compilation and imperative bootstrapping.
AI-written summary · about
chapters (10)
- 0:00Compiler verification motivation
- 5:28Proof-producing compilers
- 12:07Compiler verification approaches
- 18:56First verified compiler
- 23:13CakeML architecture and performance
- 30:18Space cost semantics
- 37:56Pure CakeML and interoperability
- 41:11Open problems in verification
- 47:23Summary of CakeML
- 48:34Q&A
related talks
43mFrom CakeML to Proof Checking, and Back Again
24mCakes That Bake Cakes: Dynamic Computation in CakeML
15mThey're the same picture: a software-verification flow adapted for hardware verification
17mPureCake: A Verified Compiler for a Lazy Functional Language
21mVerified VCG and Verified Compiler for Dafny
16mTowards formally secure compilation of verified F* programs against unverified ML(…)
50mCompCert: a journey through the landscape of mechanized semantics for verified co...
01h 06mVerifying a compiler through equational means