[11 January 2010]
Not too long ago, I wrote about cross training in programming languages, and the pleasure of rewriting things from one language into another.
Recently I had another occasion to think about that. I’ve been doing some work lately with two systems which I think of as similar, though they have different goals and emphases. ACL2 (‘a computational logic for applicative Common Lisp’) is an industrial-strength theorem prover, with a history of use for proofs of correctness for chip designs, programming languages, and mathematical propositions like the fundamental theorem of calculus. It’s a lot like a high-performance car, both in its power and in the fact that it spends a lot of time in the shop. Er, uh, I mean, it requires close, intelligent attention from the user. And its learning curve looks a lot like the approach to Mesa Verde. Alloy, by contrast, is an instance of what its designer calls “light-weight formal methods”; the language is kept simple for analysability’s sake, and no theorem prover is provided: instead, exhaustive searches through all the models of a system up to a given size are made, to find counter-examples to an assertion. It’s got a learning curve, too, but in my experience it’s pretty manageable.
I’m interested in both ACL2 and Alloy because both seem to me to offer help in making designs and specifications correct, and keeping them that way when changes are made. It would be nice to have a better sense of when one tool is more appropriate to a problem, and when the other. One conjecture I’ve entertained: Alloy for initial playing around with a design, ACL2 for fuller proofs of correctness (when real proofs are desired) after the design has settled down a bit. Solving the same problem using both tools seems like an obvious way to test that conjecture and get a sense of how the two compare.
So in a spirit of exploration, I recently took an example from the ACL2 textbook* and experimented with making an Alloy model of the same thing, which I finished the other day and have now published on the Alloy community site. The example covers a binary adder constructed from simple sub-units which add single-bit numbers. (I found it enlightening to read the Wikipedia article on adders; if you’re not an electrical engineer, you may, too.)
* Matt Kaufmann, Panagiotis Manolios, and J Strother Moore, Computer-Aided Reasoning: An Approach ([Austin]: [n.p.], 2002), section 10.5.1.
The experience poses a bit of a challenge to the conjecture just mentioned: although ACL2 does require some help proving that the relevant function terminates and that it’s correct, in some ways the ACL2 description seems simpler than the Alloy description. Certainly it’s more compact. To ensure that models are analysable, Alloy forbids recursive functions; finding an Alloy equivalent to the recursive ACL2 specification of the adder took me some head-scratching, and the result uses a lot of machinery that feels kind of ad hoc to me. But in a way, the fact that a non-recursive formulation can be found also feels like a demonstration of Alloy’s expressive power. (Short version: recursion can be changed to iteration, right? So think about using sequences.)
A really good comparative sense of the two systems will require a lot more than one exercise of this kind; ideally, I’d like a whole series of ACL2-to-Alloy and Alloy-to-ACL2 translations. Currently, my Alloy seems to be up to translating at least some ACL2 exercises into Alloy; I am not certain my ACL2 skills are up to finding ACL2 equivalents for standard Alloy exercises. If you are interested in formal methods (and who else will still be reading at this point?), all I can say is: stay tuned. And if you do any cross-translation exercises of this kind, think about sharing them!