Explicit Abstraction Barrier for Autoactive Verification
summary
Coma is a small continuation‑passing intermediate verification language that implements an explicit abstraction barrier via a hide keyword and a modal VC generator with C and D modes; moving the barrier inside the Fibonacci example (client calling fibonacci(42) and asserting >100_000_000) changes the exact proof obligations seen by caller versus definition. The implementation compiles to verification conditions, supports moving or removing barriers (no contract needed for nonrecursive functions), and is already used by a Rust deductive verifier showing the approach works.
AI-written summary · about
chapters (8)
- 0:00Autoactive verification intro
- 2:34Abstraction barriers in verification
- 3:39CoMA verification language
- 5:05Explicit abstraction barrier
- 8:05Moving abstraction barrier
- 10:37Modal VC generation
- 12:39CoMA in Rust verification
- 14:28Conclusion & Q&A
related talks
01h 01mVal: A Safe Language to Interoperate with C++
19mA Hybrid Approach to Semi-automated Rust Verification
20mModular Specification and Verification of Closures in Rust
36mThe language that isn't
57mMy favorite verbose programming technique
18mVerus: Verifying Rust Programs using Linear Ghost Types
17mRefinedRust: A Type System for High-Assurance Verification of Rust Programs
15mModular Specification and Verification of Closures in Rust