On Modelling Heap Invariants for Type Systems in Dafny

on YouTube ↗29m

" summary

Claims that a middle-level heap model can express ownership-style invariants and that Dafny can both encode and check them. Builds a prototype ~500 lines of Dafny encoding Dala-style categories (local, immutable, isolated (ISO) objects), enforces ISO reference-count ≤ 1, and validates examples like free objects and borrow-like patterns. Verification mostly works but is intermittent and sometimes opaque; some parts would be easier in Lean, while Dafny gives runnable, readable specs.

AI-written summary · about

" chapters (16)

1. 0:00Introduction
2. 0:21Key takeaways
3. 1:03Rust memory model challenges
4. 3:56Rust linked list restrictions
5. 5:44Heap model concept
6. 7:51Dafny for heap invariants
7. 9:15Syntax pitfalls
8. 10:42Semantics in heap modeling
9. 11:03Dafny heap model demo
10. 14:15Dala heap model
11. 16:02Mutable vs isolated objects
12. 18:30Islands in heap models
13. 20:58Dafny free objects demo
14. 23:47Dafny advantages and limits
15. 25:55Dafny error messages
16. 26:17Q&A