When Types are Not Enough
summary
Compares three guarantees—tests (examples), types (signatures) and proofs (for all inputs)—and shows concrete tooling: uses Isabelle proof assistant to formalize sortedness and prove insertion into a list, then exports working Scala code; demonstrates a red‑black tree invariant strategy (encode violations, balance, then prove). Presents Layon Scala verifier running on real Scala: it finds counterexamples, suggests fixes, even synthesizes implementations, uses BigInt to avoid overflow, and notes limits (no implicits/typeclass reuse by default).
AI-written summary · about
chapters (14)
- 0:00Start
- 2:24What Is Software Development
- 3:51What Are Specifications
- 6:48The Proof Level
- 8:16Kurihara Isomorphism
- 12:34Proof Systems
- 16:33Implement an Insertion Sort
- 19:02Evaluate Function Calls
- 19:49Inductive Predicate
- 27:18The Code Generator
- 28:31Insert Function
- 29:25Export Haskell
- 34:15Size Function
- 36:06Insert Function Example
related talks
46mTesting in the world of Functional Programming
19mCovering All the Bases: Type-Based Verification of Test Input Generators
48mPROBING THE UNPROVABLE AND PROVING THE IMPROBABLE
45mTDD, as in Type-Directed Development
36mTesting for Lawful Good Adventures
01h 00mA New Approach to Testing with ScalaCheck / Property Based Testing
44mTypes and Property Tests for Software Resiliency
18mType-Based Incorrectness Reasoning