Comment by peterbotond

Racket is a programming language programming language to program and prove programming languages. See eopl. (edit: yes it is a pun and a brain twister. i love racket (and scheme too))