Keynote
summary
Dafny adds a boogie extractor that proves models for sets, sequences and multisets and emits Boogie axioms (it already caught a faulty multiset axiom), an auditor that flags incorrect foreign‑function interface specs (Java, JavaScript, Go, Python, C, Rust), and project files plus a verb‑style CLI. The type inference is fully reimplemented and used at AWS for over a year. CAN calls become the sole mechanism for unfolding, fuel encoding is redesigned to avoid quadratic unrolling, and work uncovers and helps fix Z3 bugs.
AI-written summary · about
chapters (15)
- 0:00Daphne language keynote
- 12:22Testing tools in Daphne
- 17:42Language features overview
- 21:15Type inference in Daphne
- 27:00Subset types and constraints
- 36:20Type checks and conversions
- 40:38Proof brittleness challenges
- 46:22Proof organization improvements
- 51:21Allocatedness and mutable state
- 1:00:14New language features wish list
- 1:14:28Open design questions
- 1:19:01Future of Daphne
- 1:20:24Fuel encoding improvements
- 1:23:10Boogie extractor for axioms
- 1:25:17Q&A
