Proof Theory Impressionism: Blurring the Curry-Howard Line
summary
Claim: bridge the gap between program and proof by extracting denotational semantics from Rust into a dependently typed checker. Uses Rust type-level naturals and type-indexed vectors to encode sizes, encodes state-machine protocols at the type level, and aims to emit Agda specifications that the Agda type-checker can verify. Demonstrates ugly extracted C from Coq as a caution, shows a prototype tool that parses Rust syntax to produce Agda specs, and admits the mechanized extractor and full automation are work in progress rather than solved.
AI-written summary · about
chapters (8)
- 0:00Start
- 3:13Sensor Fusion
- 9:10Denotational Semantics
- 10:45Inference Rule for a Type Theory
- 11:56Dependent Type Theory
- 17:02Dependent Types
- 24:29Operational Semantics
- 30:15Creation of the Adjacency List
related talks
41mWar Time Proofs and Futuristic Programs
01h 16mCoding Agents: New opportunities for formal methods?
11mWhat are Dependent Types
01h 44mAn Introduction to Natural Deduction
38mAutomatically Synthesising Programs that We Can Trust
10mWhen Does a Program Typecheck?
26m(...) How to turn (Liquid) Haskell into a theorem prover
29mRust is the language of the AGI