In Types We Trust
summary
Argues that stronger contracts come from types and proofs rather than only examples, implements a Scala sealed ADT for natural numbers with a recursive +, runs property-based tests (generator limited to 0–100, printing edge cases like 100 and 101) that pass, then sketches an inductive proof of associativity and shows the same proposition encoded in dependent types (Agda/Idris) so a compiled inhabitant is a unit proof guaranteeing the property.
AI-written summary · about
chapters (18)
- 0:00Introduction
- 0:43Eiffel
- 5:07Require
- 6:20Testdriven development
- 9:54Hope faith and proof
- 13:14Natural Number
- 14:54Scala
- 18:19Writing a test
- 21:35Faith and proof talk
- 23:17Proof example
- 25:29Proof algorithm
- 27:49Proof algorithm 0
- 36:24Proof framework
- 37:14Contract
- 39:10Unit Tests
- 39:34Scala Center
- 40:15Questions
- 41:06Proof
related talks
37mIn Types We Trust
52mWhat logic can teach us, Scala programmers
30mDotty and types: the story so far
45mTypelevel Programming 101: The Subspace of Scala
37mWhen is an ADT not an ADT?
48mAcademese to English: A Practical Tour of Scala’s Type System
19mLogically Qualified Types for Scala 3
47mIdris For (Im)practical Scala Programmers