A little goes a long way

I just completed an automated, machine-checked simulation proof. What was my proof assistant? Scheme! The proof relies on some reduction relations and an inductively defined invariant relation. The former can be defined in PLT Redex with just a little cleverness for performing symbolic reduction; the latter can be defined with good, old-fashioned recursion.

Granted, there are a number of places where I could have gone wrong. For example, I have no meta-theorems about the correctness of the representation or the exhaustiveness of the manually directed case analysis (a dozen cases in as many lines of code). But implementing the proof on the computer helped me debug a number of minor issues in my theorem, and it did all the heavy lifting for me (particularly the multi-step reductions--thanks Robby and Jacob for PLT Redex!).

The moral? A little goes a long way, as Wand and Sullivan wrote. For a simple proof involving inductive invariants and lots of rote calculation, there's no need for complicated meta-logical frameworks. Implementing the proof in a general-purpose programming language gives you a higher degree of quality assuredness for a reasonable implementation cost.

Next, if I do more of these simulation proofs, I might start abstracting out the common patterns into a library to work in conjunction with PLT Redex. It would essentially be a simple proof assistant for simulations.