Random Testing for Functional Programs
Testing in functional programming languages often uses property-based testing, where properties that functions should satisfy are specified. Haskell’s QuickCheck library automates this process by generating random test inputs and checking whether the properties hold, making it easier to discover subtle bugs and edge cases.
Goals
Reimplement QuickCheck in Lean to extend formal verification and theorem proving by property-based testing and automated test generation.