In Types We Trust
summary
Proposes expressing semantic contracts as predicate-logic statements that feed both property-based tests and machine-checked proofs and shows concrete support in ScalaTest + ScalaCheck. Implements Peano naturals (sealed trait zero/successor), writes plus, and runs generators bounded 0–100 so hundreds of random combos pass (examples like 31,34,62 printed). Then gives an inductive proof of associativity using the actual implementation rewrite rules (0+R = R, succ(P)+R = succ(P+R)), arguing proofs are hard but feasible and types should carry contract faith.
AI-written summary · about
chapters (7)
- 0:00Introduction to design by contract
- 2:06From Eiffel to Java and tests
- 8:28Natural numbers in Scala
- 12:37Testing associativity of addition
- 16:42Science vs. proofs in programming
- 25:27Formal specs with types and tests
- 28:59Q&A session
