Theorem provers are a P.L. researcher's best friend
summary
Argues that mechanized proof shifts PL research from handwavy claims to verifiable artifacts, showing concrete use of Coq and Isabelle/HOL plus SMT solvers to formalize languages, type systems and optimizers; demonstrates a CompCert-style correctness proof for a compiler from arithmetic expressions to a stack machine and shows it executes and preserves semantics; cites large verified projects (seL4, VST, Iris, EverCrypt) and estimates ~25% of PL papers now ship machine-checked proofs.
AI-written summary · about
chapters (13)
- 0:00Research trends in PL
- 1:20Evidence in research
- 2:55Soundness and metatheory
- 4:31Tension in proof writing
- 7:19Automatic theorem provers
- 9:29Interactive provers
- 12:46Mechanized proofs as a game
- 13:53Compiler verification demo
- 17:19Stack machine implementation
- 22:41Proof of correctness
- 27:16Real-world projects
- 30:21Impact on PL research
- 33:41Q&A and discussion