In the testing I focus on, testing of compilers, and in particular Common Lisp implementations, PBT has been invaluable, finding bugs in every implementation on

In the testing I focus on, testing of compilers, and in particular Common Lisp implementations, PBT has been invaluable, finding bugs in every implementation on which it was tried (I understand this is a universal experience in compiler testing, for example seen from Csmith on C compilers). Here, the property is often of the form "these two related pieces of code should not crash and also compute the same thing". As a simplified example, an expression like (+ x y) should compute the same thing as (the <type1> (+ (the <type2> x) (the <type3> y))) where the types are randomly generated types that contain the values in question.