Metaprogramming, Synthesis & Verification • Nada Amin • YOW! 2025

This presentation was recorded at YOW! Australia 2025. #GOTOcon #YOW https://yowcon.com Nada Amin - Assistant Professor of Computer Science at Harvard SEAS RESOURCES https://github.com/namin https://www.linkedin.com/in/mitnamin https://cv.namin.org Links https://namin.seas.harvard.edu https://github.com/namin/dafny-sketcher https://github.com/namin/staged-miniKanren https://github.com/namin/llm-verified-with-monte-carlo-tree-search https://github.com/namin/holey https://github.com/metareflection/dafny-annotator https://github.com/namin/eurisclo https://io.livecode.ch/learn/gregr/icfp2017-artifact-auas7pp ABSTRACT 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, multi-stage miniKanren, VerMCTS, and Holey. [...] TIMECODES 00:00 Intro 00:14 Verified synthesis 02:04 Neurosymbolic spectrum 03:14 Verification with Dafny 05:25 Demo 17:52 Orchestrating program synthesis 18:55 VerMCTS setup: Verified programming 20:41 PUCT 22:33 Dafny Sketcher 27:06 Holey 29:29 Demo 30:20 Lessons from Holey 31:15 Relational programming 33:22 Demo 35:46 Takeaways 37:27 Outro Download slides and read the full abstract here: https://yowcon.com/brisbane-2025/sessions/3919 RECOMMENDED BOOKS Forsgren, Humble & Kim • Accelerate: The Science of Lean Software and DevOps • https://amzn.to/3tCz1xO John Arundel & Justin Domingus • Cloud Native DevOps with Kubernetes • https://amzn.to/3hKZvI5 Wynne, Hellesoy & Tooke • The Cucumber Book • https://amzn.to/3tEUINJ https://bsky.app/profile/gotocon.com https://twitter.com/GOTOcon https://www.linkedin.com/company/goto- https://www.instagram.com/goto_con https://www.facebook.com/GOTOConferences #Metaprogramming #Synthesis #Verification #VerMCTS #Dafny #MonteCarloTreeSearch #DafnySketcher #miniKanren #Holey #RelationalProgramming #NadaAmin #YOWcon CHANNEL MEMBERSHIP BONUS Join this channel to get early access to videos & other perks: https://www.youtube.com/channel/UCs_tLP3AiwYKwdUHpltJPuA/join Looking for a unique learning experience? Attend the next GOTO conference near you! Get your ticket at https://gotopia.tech Sign up for updates and specials at https://gotopia.tech/newsletter SUBSCRIBE TO OUR CHANNEL - new videos posted almost daily. https://www.youtube.com/user/GotoConferences/?sub_confirmation=1