MetaCoq as a tool to prevent future unsoundness in Coq
summary
MetaCoq formalizes Coq’s calculus inside Coq and provides verified implementations of core pieces of the kernel, aiming to catch soundness bugs before they reach the ~18k‑line OCaml kernel that historically yields about one critical bug per year. The project (12 core contributors, begun 2014) already produces a sound and complete type checker (slow but correct), proved standardization assuming strong normalization, and found a real case‑analysis bug in cumulative inductives that required a year of representation changes to fix. Roadmap: a verified kernel run in CI and extraction via LambdaBox and Malfunction with a machine‑checked pipeline to OCaml.
AI-written summary · about
chapters (16)
- 0:00Intro
- 1:03What do you trust?
- 2:26The underlying type theory, according to the manual
- 3:10Papers and PhD theses
- 4:49The ideal of proof assistants
- 6:59The trusted core
- 17:04Types of truth in proof engineering
- 18:53Weak call-by-value standardisation
- 19:49Consistency and strong normalization
- 21:57A sound and complete type-checker
- 23:23A success story
- 30:08Issues with implementation of extraction
- 31:15The vision
- 34:57Verified Extraction to Malfunction
- 37:50Free results
- 38:24Todo-Lists
related talks
01h 03mVerifying Dependent Type-checkers
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
31mA Coq Library of Undecidable Problems
24mCode Extraction from Coq to ML-like languages
59mCoq to C Translation with Partial Evaluation + Counterexample Generation
21mVerified Extraction from Coq to OCaml
36mMcTT: Building A Correct-By-Construction Proof Checker For Martin-Loef Type Theory
24mConCert: A Smart Contract Certification Framework in Coq