Contracts For Getting More Programs Less Wrong
summary
Explains how executable contracts (using JML and the CMU teaching language C0) move tests toward full correctness by enforcing preconditions, postconditions and loop invariants at runtime, teaching students to prove code like the Fibonacci loop invariant and catching a real-world java.utils.Collection.sort bug fixed via a theorem prover, shows contracts run in debug only and can double-check every call and document precise specs that compilers and provers can use.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 0:45The Leap
- 5:51The Gap
- 11:50The First Takeaway
- 17:18Contracts in Functional Languages
- 20:39Fibonacci
- 22:18Writing Fibonacci
- 30:03Loop invariant
- 34:20Compile time guarantees
- 35:17Timsort
- 35:45Conclusion
related talks
01h 34mKeynote: Contracts, Testing & the Pursuit of Well Defined Behaviour
43m(Programs), Proofs and Refutations (and Tests and Mutants)
29mBeyond Unit Tests: Taking Your Testing to the Next Level
01h 06mDefensive Programming Done Right, Part II
37mBreaking the bank with test contract
14mSynthesizing Contracts Correct Modulo a Test Generator
18mPreview: Verification (Correctness)
32mDesign by Contract in Elixir(...)