J. Strother Moore, the Moore in Boyer-Moore, just completed a two-days visit to Northeastern. He gave a talk, Machines Reasoning about Machines, complete with demo using the ACL2 theorem prover. ACL2 is a first-order theorem prover for proving equational properties of programs written in an applicative subset of Common Lisp. It is amazingly fast, and comes with a well-equipped library of theories to work with.
Fascinating work, if only because I am set to teach an undergraduate course using ACL2 next semester with Pete Manolios.
Now if we could just move the ACL2 technology to a typed language and extend it to higher-order, I'd be happy. (I know, I know, there are fundamental limitations re the latter, but still, even getting halfway there would be fun.)
Pete told me that the two books on ACL2:
- Computer-Aided Reasoning: An Approach
- Computer-Aided Reasoning: ACL2 Case Studies
are now available in paperback for a very reasonable fee.