37:32

With live examples Nada 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).