Abstract
Most software engineers spend much time testing and little time proving; most "semantics engineers," on the other hand, spend much time proving and little time testing. Bringing formal methods into the mainstream of software engineering is a long-standing goal, but there have been relatively few efforts to leverage conventional software engineering techniques in the formalization of programming language semantics.

This talk describes the use of one such technique, randomized test case generation, in PLT Redex, a domain specific language for specifying and debugging operational semantics. In keeping with the spirit of Redex, the language's randomized testing support is as lightweight as possible---the user encodes a conjecture as a predicate over the terms of the object language, and Redex attempts to produce a counterexample automatically.