Type-level Property Based Testing
summary
An automated framework in Idris 2 runs type-level QuickCheck during compilation to test dependent-type models built as an indexed state monad. Properties generate traces (100 random tests by default), find a counterexample showing the ATM stays in CardInserted within 10 steps, and after adding a retry-with-eject rule the property passes (100/100). The approach uses dependent pairs to generate indexed values, emits failing traces in the REPL, and currently uses a fixed compile-time random seed.
AI-written summary · about
chapters (9)
- 0:00Type-level PBT intro
- 1:27Verification spectrum & stateful systems
- 3:36Dependent types for state machines
- 7:10Challenges in dependent types
- 9:59ATM operations with QuickCheck
- 11:02Idris 2 & QuickCheck testing
- 13:32Unified spec & implementation
- 15:19Testing type-level programs
- 16:06Q&A
related talks
23mProperty based testing is a mindset
14mVerify, but test: extracting property-based tests from F* specifications
42mSurprise yourself with Property Based Testing
46mTesting in the world of Functional Programming
01h 00mA New Approach to Testing with ScalaCheck / Property Based Testing
25mPowerful Testing with test.check
36mProperty Based Testing: From Theory to Practice
01h 24mIntroduction to Property Based Testing