Programmable Property-Based Testing
Property-based testing (PBT) is a popular technique for establishing confidence in software, where users write executable specifications that are checked many times by a testing framework. In modern PBT frameworks, properties are typically written in shallowly embedded domain-specific languages, tightly coupled to the testing process. We propose a new, deeper language for properties based on a mixed embedding called deferred binding abstract syntax, which reifies properties as data structures and decouples them from the property runners that execute them. We implement this language in Rocq and Racket, leveraging dependent and dynamic types, respectively, and showcase its flexibility by rapidly prototyping various property runners, highlighting domain-specific testing improvements unlocked by more programmable testing.
Such frameworks often provide convenient configuration options to customize aspects of the testing process, but users are limited to precisely what library authors had the prescience to allow for when developing the framework; if they want more flexibility, they may need to write a new framework from scratch.