Dependent Types to Push Corners of the Property-based Testing (Extended Abstract)
summary
Generates dependently-typed inputs from Idris specifications to fuzz a TypeScript-like compiler and interpreter, using a partly derived dep_check library generator pipeline and Idris encodings of syntax and contexts; a 300-line spec plus derived generators exercises JIT optimizer, typechecker and codegen and exposes many subtle crashes and type errors that handwritten tests missed; generators are indexed for emptiness to avoid runaway backtracking and deliver practical completeness and distribution guarantees.
AI-written summary · about
chapters (9)
- 0:00Dependent types and property testing
- 1:02Type-driven meaning
- 2:24Sorted lists with dependent types
- 5:42Testing TypeScript-like language
- 9:44Bugs via property-based testing
- 12:12Generator challenges for dependent types
- 16:48Complete generator derivation
- 17:54Summary
- 18:16Q&A
related talks
28mLanguage Support for Property-Based Testing
19mCovering All the Bases: Type-Based Verification of Test Input Generators
39mTDD as in Type-Driven Development
30mProperty-based Testing for Godly Tests
26mThe missing piece of testing
36mProperty-Based Testing: Unveiling the Truth on Test Reduction
23mProperty based testing is a mindset
01h 24mIntroduction to Property Based Testing