A Galilean revolution for computing
summary
Claim: computation achieves unboundedly scalable reliability and efficiency by making correctness machine-checkable and compositional. Approach uses dependent types and Agda proofs to encode denotational specifications (example: parsing via language derivatives with machine-checked lemmas and a working Agda parser/proof), rejects operational/monadic IO as lossy, and pushes for proof-driven hardware design. Reported efficiency gain target is 1k–10k× efficiency by abandoning sequential instruction models; exact real arithmetic and error-bounded floats with proofs are proposed as practical routes.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 3:52Galilean revolution for computing
- 18:35Wrong computing foundation
- 20:18Opportunity in logic and computation
- 23:07Correctness for scalability
- 28:24Compositionality and specifications
- 34:05Haskell’s role and limits
- 47:02Dependent types and correctness
- 59:27Q&A on machine learning
- 1:06:44Teaching new informaticians
- 1:13:29Complex specs and hardware
- 1:22:39Floating point and exact computation
- 1:27:12Closing and Q&A
related talks
47mHow to trust a verified program?
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
01h 07mThe Cogent and Dargent approach to facilitating verified software development
19mPete's Footprints
21mMechanised Hypersafety Proofs about Structured Data
58mA New Perspective on Commutativity in Verification
24mIncremental Computation: What Is the Essence? (Invited Contribution)
01h 05mVerifying Infinitely Many Programs at Once