Living inside a Theorem Proving Universe
summary
Talk argues for working entirely inside a theorem prover by embedding other logics, languages and tools and shows concrete wins and costs. Examples include embed the B method in PVS in about 25–30 lines, capture the Boogie memory model in 20–25 lines, and reprove hard results in a night or run major proofs in “lunch” (30–90 minutes); code generation to C, rich type info (e.g. positivity for factorial), and a 16,000-line verified development appear alongside usability and maintenance burdens.
AI-written summary · about
chapters (17)
- 0:00Introduction
- 1:05Living in a theorem prover
- 3:53Mechanized theorem history
- 8:52Automated proving breakthroughs
- 12:25Sap-off hypothesis language impact
- 15:53Formalization errors type benefits
- 18:24Theorem provers beyond proof
- 20:30Embedding logics and languages
- 22:38Why live inside a prover
- 25:07Proving limitations challenges
- 28:191995 case revisited
- 30:27Semantic integration benefits
- 31:54Modeling in prover ecosystem
- 32:57Conclusion future of proving
- 35:07Q&A: Choosing a prover
- 36:18Q&A: LLMs and theorem proving
- 39:11Q&A: Bridging formal-informal gap
related talks
01h 34mFormal Logic Undressed
31mLetting users do the undecidable: lessons from program synthesis
57mResearch on Different Time Horizons (and an Example with Machine-Checked Proofs)
19mPanel: Compilation Frameworks
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
21mVerifying term graph optimizations using Isabelle/HOL
53mSemantics-based program manipulation in the age of LLMs
46mRefinement Types from Light to Deep Verification