How to trust a verified program?
summary
Proof assistants like Agda, Coq and Lean still permit real failures: a universe overflow caused by 63-bit integer wrap lets Agda accept falsity; a positivity/recursion lapse and aggressive GHC inlining can crash compilers or produce divergent behavior; Coq-to-Haskell extraction mismatch flips constructors and turns a proven-safe function into a runtime error. The project building a certifying pipeline for Plutus TX emits ASTs for each pass, checks a formal translation relation between steps, and uses contextual equivalence to ensure compiled code preserves semantics.
AI-written summary · about
chapters (16)
- 0:00Intro
- 3:01Program verification in a nutshell
- 5:04Specifications
- 7:21Programming and proving
- 8:40Theoretical problems in type theory
- 11:26Implementation problems
- 14:23Another theoretical problem...
- 15:56Implementation consequences...
- 18:01Type theory - a language for programs & proofs - in theory...
- 19:29Problems with transpilation
- 27:07Compilation may change semantics
- 29:35Certified compilation for smart contracts
- 31:42Specifying the compiler: translation relations
- 33:44Example: inlining
- 36:44Certification
- 41:18Perspectives for trustworthy verified programs
related talks
01h 05mVerifying Infinitely Many Programs at Once
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
30mTrustworthy Runtime Verification via Bisimulation
16mTowards formally secure compilation of verified F* programs against unverified ML(…)
01h 04mCoq's vibrant ecosystem for verification engineering
01h 02mLanguage Design meets Verifying Compilers
21mMechanised Hypersafety Proofs about Structured Data
15mTowards Verifying Crash Consistency