PLT Redex is a tool for the researcher working with programming languages, operational semantics, type systems, program analyses, and so forth. It is a domain-specific language in Racket designed after the notation found in research papers. You can find great documentation and educational materials about PLT Redex, but they tend to assume that you are already familiar with programming-language theory. When I was learning about PLT Redex, I was new to both the tool and to programming-language theory, so sometimes I struggled to follow along. What I found, however, is that it can be a two-way street: learning PLT Redex has helped me understand papers and programming-language theory.
This article is targeted at people in a similar place. We introduce PLT Redex for the reader new to programming-language theory, avoiding Greek letters and jargon. We (ab)use the tool to play a game of Peg Solitaire and explore the features for functional programming, pattern matching, contract verification, nondeterministic computation, visualization, typesetting, test generation, and so forth. It is a fun exercise of repurposing a tool for tasks beyond its intended design, and a first step for reading technical papers.
We start by reviewing Peg Solitaire rules. We model the game in PLT Redex in a series of steps. Pegs and boards become terms, and we learn how to pattern match on them. We specify a language to determine what terms represent pegs and boards, and define metafunctions and predicate relations over them. We proceed to more sophisticated features for nondeterministic computation: judgment forms and reduction relations. We then use visualization tools to play Peg Solitaire. We glance at other features, including test generation and typesetting. Finally, we discuss PLT Redex limitations, related work and conclude.