Incremental Proof Development in Dafny with Module-Based Induction
summary
Claim: encoding Coq-style induction principles as module-based induction in Dafny makes iterative proofs stable and debuggable. Implementation: a list induction module pattern and analogous principles for a mini-Dafny interpreter (the interpreter is ~1,000 lines) are used so updates force only tiny, local lemmas to re-prove. Applied across a ~10,000 LOC compiler development, proofs like associativity, a purity lemma, a zero-multiplication pass, and a val-change check go through automatically once the induction structure is fixed, and failing lemmas surface immediately, keeping verification fast and maintainable.
AI-written summary · about
chapters (8)
- 0:00The challenge of verification
- 1:54Induction and proof failures
- 6:28Implementing induction modules
- 8:26Compiler verification context
- 8:54Case study: Mini-Dafny
- 9:12Automation and usability
- 13:26Audience Q&A
- 15:03Future automation potential
related talks
15mOn the Impact of Formal Verification on Software Development
21mLive Verification in an Interactive Proof Assistant
29mType Inference Techniques: Implementation and Formalization, Better Together
13mA Drag-and-Drop Proof Tactic
25mIncremental Type-Checking for Free: Using Scope Graphs to Derive Incremental Type-Checkers
01h 10mMedium-scale automation for proof assistants
24mCode Generation via Meta-programming in Dependently Typed Proof Assistants
22mInducTeX: A MetaCoq plugin for typesetting inductive definitions