Language Design meets Verifying Compilers
summary
Compares two real verifying-compiler languages and shows concrete trade-offs: Dafny+Boogie+Z3 lets the verifier replace typing (flow typing, interpreted vs uninterpreted functions) and can prove an unreachable assert in an Ethereum deposit snippet that holds ~9 million ETH; Whiley separates typing and verification, forcing explicit asserts/failed statements and different loop-invariant strategies. Presents a 6k-line Dafny EVM executable spec that CI re-verifies, contrasts purity/mutable-value optimizations, and stresses need for good counterexamples when Z3 times out.
AI-written summary · about
chapters (17)
- 0:00Introduction
- 0:34Background
- 3:47History
- 5:10Stanford Pascal
- 6:09Tony Hall
- 8:10Solidity Deposit Contract
- 10:54Ethereum Virtual Machine
- 12:10Daphne Wiley
- 14:36Verifying Compilers
- 16:41Compiler Pipeline
- 20:24Daphne
- 27:11Flow typing
- 31:06Functional Purity
- 36:36Uninterpreted Functions
- 44:20Open Statement
- 44:50Inference
- 52:25Questions
related talks
19mLean on Dafny: Exploring Interactive Verification of Dafny Programs in Lean
21mVerified VCG and Verified Compiler for Dafny
15mOn the Impact of Formal Verification on Software Development
41mBattle of the Languages
19mVerifying Dafny Contract Integrity
01h 05mAll the Languages Together
01h 06mVerifying a compiler through equational means
01h 05mMuch Still to Do in Compiler Verification (A Perspective from the CakeML Project)