Trying to prove something in Coq is like operating a large, fly-by-wire bulldozer. On the one hand, you have to figure out what to shove where, or how to program the machine to do the shoving for you. On the other hand, you can use your superior human pattern-recognition skills to avoid driving into obstacles, and if you do get stuck, you have at least some chance of figuring out how to extricate yourself.
Trying to prove something in ACL2 is like imperiously proclaiming, “Robot servants, hear my command!” and then they run out into the junkyard picking up stuff and moving it around. And if you're lucky, and the task you've given them simple enough, they get the job done for you while you sit back on a lounge chair sipping a strawberry daiquiri. But if that's not the case, they run around doing exactly the wrong thing, until either they explode messily of their own accord or you call in an airstrike. And then you get to examine the flaming wreckage to figure out what went wrong, and what helpful hints you might be able to offer the robots next time.
No comments:
Post a Comment