Research on Different Time Horizons (and an Example with Machine-Checked Proofs)
summary
Argues that long-horizon long-term systems work pays off by combining judgment with iterative prototyping, demonstrates end-to-end mechanized proofs using Coq and a verified stack (hardware to application) via a real verified IoT light bulb prototype, and describes Fiat Cryptography: a Coq-verified generator that produces C/assembly matching hand-tuned performance (several× faster than GMP, ~2× behind best asm in one case) adopted into browsers (Chrome in 2018); main bottleneck is proof-checking time.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 1:18Proof assistants in PL research
- 3:47Cognition and time horizons
- 10:48Short vs long research
- 14:00End-to-end mechanized proofs
- 21:32Verifying compilers
- 32:45Fiat cryptography
- 41:12Google adoption
- 42:15Formal verification bottlenecks
- 44:40Hardware-software interfaces
- 50:00Summary and future
- 50:47Q&A
related talks
56mProof Assistants At the Hardware-Software Interface
58mFast Cryptographic Code via Partial Evaluation
41mLiving inside a Theorem Proving Universe
23mSmooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs(…)
24mFormally Verified Native Code Generation in an Effectful JIT: Turning the CompCe...
29mTowards Formally Verified Just-In-Time Compilation
19mFormally Verifying Optimizations with Block Simulations
01h 23mProgram Presentations