Quod Erat Covered-In-Bees

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.

This Morning's Compiler Meditation:

translating Knuth's “man or boy” test from ALGOL 60 into C, by reifying the activations as structs and closure-converting the call-by-name thunks. Like this.

I considered trying to run it by hand instead, but that would certainly take a lot of paper, and also as Knuth himself apparently failed in that task, I thought perhaps not.