How to Trust a Verified Program - Challenges and Solutions in Program Verification

Explore the challenges and pitfalls of trusting verified programs in this 47-minute ACM SIGPLAN conference talk. Delve into the world of proof assistants based on type theory, such as Agda, Coq, Idris, and Lean, and their role in establishing program correctness. Examine the conceptual promise of reducing the trusted code base and the practical reality of verified programs still failing. Investigate various ways in which these programs can go wrong and potential preventive measures. Cover topics including program verification basics, specifications, programming and proving, theoretical problems in type theory, and implementation issues. Analyze the challenges of type theory as a language for programs and proofs, problems with transpilation, and the impact of compilation on semantics. Explore certified compilation for smart contracts, specifying compilers through translation relations, and the process of certification. Gain insights into the future of trustworthy verified programs and the ongoing efforts to bridge the gap between theory and practice in program verification.

Intro
Program verification in a nutshell
Specifications
Programming and proving
Theoretical problems in type theory
Implementation problems
Another theoretical problem...
Implementation consequences...
Type theory - a language for programs & proofs - in theory...
Problems with transpilation
Compilation may change semantics
Certified compilation for smart contracts
Specifying the compiler: translation relations
Example: inlining
Certification
Perspectives for trustworthy verified programs