Metaprogramming, Synthesis, and Verification
Friday Dec 5
13:15 –
14:00
Blue Room
With live examples I will demonstrate:
- Dafny and verification-aware programming, including proof by induction to verify properties of programs (for example, that an optimizer preserves semantics).
- Multi-stage programming, a principled approach to writing programs that write programs, and its incarnation in multi-stage relational programming for faster synthesis of programs with holes—with the theoretical insight that a staged interpreter is a compiler, and a staged relational interpreter for a functional language can turn functions into relations running backwards for synthesis.
- Monte Carlo Tree Search, specifically the VerMCTS variant, and when this exploration-exploitation sweet spot is a good match for synthesis problems.
The ideas will be demonstrated with live examples and open-source artifacts spanning verified programming, relational programming, and LLM-guided synthesis, including Dafny Sketcher (https://github.com/namin/dafny-sketcher), multi-stage miniKanren (https://github.com/namin/staged-miniKanren), VerMCTS (https://github.com/namin/llm-verified-with-monte-carlo-tree-search), and Holey (https://github.com/namin/holey).
