Building the systems of tomorrow
summary
Claims that Idris and dependent types plus total functional programming can eliminate whole bug classes, and shows concrete evidence: government unemployment system that sent €25M too much, Night Capital losing $440M in 30 minutes, Toyota acceleration causing 89 deaths, a radiotherapy bug killing 17 and a plane crash killing 154. Demonstrations include vects enforcing lengths, Curry–Howard as types-as-proofs, totality/termination checking, modeling servers as streams and property-based testing as a fallback.
AI-written summary · about
chapters (39)
- 0:00Who am I
- 2:54Knight Capital Group
- 3:17Apple
- 3:30Heartbleed
- 3:58Radiotherapy
- 4:30Toyota
- 4:52Spanair
- 5:14correctness matters
- 5:32why are there so many bucks
- 5:52our tools
- 8:03bicycles
- 8:43implicit assumptions
- 9:16turing machine
- 9:39lambda calculus
- 10:08theorems and proofs
- 11:02propositional logic
- 12:23use essence
- 12:54apples
- 13:19function types
- 14:40cardinality
- 15:07card analogy
- 15:50list analogy
- 16:17list examples
- 16:41a controversial example
- 16:51the cardinality
- 17:39two lists of eight
- 17:59tool belt dependent types
- 18:32low cardinality
- 19:16short type checks
- 20:12proof
- 22:12total functional programming
- 22:52termination and productivity
- 24:12Turing completeness
- 24:31Propertybased testing
- 25:18Recap
- 26:02A little bit experimental
- 26:28The goal
- 27:47Questions
- 27:59Practical Applications
related talks
21mLearning to Love Type Systems
34mTypes Are Not Safe
21mBeyond Type Checking Building Bulletproof TypseScript Applications
38mType Systems - The Good, Bad and Ugly
39mTDD as in Type-Driven Development
36mCommunicating in Types
47mHistory and Philosophy of types
01h 01mDeconstructing TypeScript’s Type System