Run Your Research in Racket

One of the most fun talks at the Principles of Programming Languages (POPL) conference this year was about Redex, a Racket-based system for lightweight mechanization of programming language semantics. This system allows people to encode their language semantics and theorems in the Racket programming language (the new face of Scheme). The programmer can then play with example programs evaluated using these semantics and use random testing to validate their theorems. This is a much lighter-weight alternative for getting formalisms right than using interactive proof assistants such as Coq. You may read more on the project website.