One way to eliminate flaws from a model is to write it down in a mechanized formal language. It is then possible to state theorems about the model, to prove them, and to check the proofs. Over the past nine years, PLT has developed and explored a lightweight version of this approach, dubbed Redex. In a nutshell, Redex is a domain-specific language for semantic models that is embedded in the Racket programming language. The effort of creating a model in Redex is often no more burdensome than typesetting it with LaTeX; the difference is that Redex comes with tools for the semantics engineering life cycle.
In this paper we report on a validation of this form of lightweight mechanization. The largest part of this validation concerns the formalization and exploration of nine ICFP 2009 papers in Redex, an effort that uncovered mistakes in all nine papers. The results suggest that Redex-based lightweight modeling is effective and easy to integrate into the work flow of a semantics engineer. This experience also suggests lessons for the developers of other mechanization tools.
Paper (in pdf)
Redex models
POPL 2012 Talk Video:
on youtube
Talk
source code and slides (but the paper is easier to read than the slides).
Also see the project website.
Redex is available as part of the main Racket download.