It’s dangerous to go alone take Church-Rosser Theorem

I was at work the other night, getting my feet wet for the first time with a tool that’s known an automated proof assistant.  Now there’s no need to go into all of the details of an automated proof assistant (or of Coq, the specific tool I was using.  Incidentally, none of this is really specific to Coq.  I just wanted a reason to include a picture of a French rooster in a white suit) to get something out of this post, which should after all, be talking about video games at some point, but the basic idea is something like this.  A mathematical theorem isn’t taken for true in mathematics until it has a complete, fully-hashed out proof that should be a beautiful model of objective perfection.  But that’s kind of BS, because in reality, a proof boils down to an argument (albeit a very careful one) that convinces enough mathematicians, and for which the other ones can’t find a flaw.

Coq makes the ideal of objective perfection in proofs a reality.  If you have some theorem in mind, then you write it up in the language of Coq, and then you do the same for the theorem’s proof.  The key feature of Coq is that never lets you off the hook when you’re writing your proof.  Each step has to follow the established rules, or it doesn’t let you take the next step.  This is why Coq is sometimes viewed as “needlessly formal and pedantic,” and keep in mind this is coming from a group of people that see articles with titles like Round-Efficient Broadcast Authentication Protocols for Fixed Topology Classes and lick their lips with excitement. So it was at least a little surprising to me that as I was sitting there hacking away with this thing, and I was actually having fun in the process. And not just “fun” in the sense of “pretty fun as far as educational software goes”: I realized that something about this felt like gaming back in the 8-bit days: a little like Zelda or Ninja Gaiden for some reason.  This got me thinking on just what I loved about those old games, or good games from any time, that could possibly overlap with something like a proof assistant.  I think it boils down to the following.

First, I have a hunch that people (and this includes kids playing old NES platformers) can really enjoy doing something that’s demanding and rigorous, as long as they don’t feel like they’re being cheated. Ask someone what math course they hated the most in high school, and a large amount of the time it seems like the answer is “geometry.” For a mathematician, that’s a pretty depressing answer to hear, because high school geometry is supposed to be everyone’s first introduction to the notion of formal proof. But is it really?  Sometimes for me it felt like a few steps of a proof intuitively “worked” for the teacher but other steps, indistinguishable to me from the good ones, were no good, and I could never get a clear answer why. But consider that kids a lot younger than high-schoolers do something that arguably takes a lot more dedication than geometry whenever they play through Ninja Gaiden, yet they do it willingly.  In their own free time.  Why?  Personally, part of the reason I slogged through that cruel, cruel game was because even though so many of the victories were so hard-won, you knew that when you beat friggin Stage 6-4, then that win was really yours, not caused by the whim of the game spontaneously not liking the way you plaed or deciding to finally go easy on you.  I think a lot of the satisfaction of working with Coq stems from the same thing.  Coq doesn’t give you any breaks, so getting practically anything done is a huge pain.  But when you finally prove the theorem that you set out to prove, it makes your sense of satisfaction that much more complete.

Second, working with Coq gives you satisfaction in incremental pieces. You have an overall goal (to prove your theorem), but to get there, Coq forces you to break your goal down into subgoals, and further subgoals until you can handle your task one chunk.  Each time you prove a subgoal (or lemma), the background color of your environment resolves to a pleasing shade of blue, and the system prints a gratifying “Subgoal proved.  Lemma definition added.”  It’s a very “Shine Get” moment.  Now that you’ve put in the work to prove the lemma, its yours to use as a tool as you see fit for the remainder of your task.  So maybe Zelda or Megaman are better analogies than Mario.

Above: a typical Coq session, mid-proof.  In the top frame, text in blue has been checked by Coq.  In the bottom, text below the “====” gives your current subgoal, and text above the “====” gives the hypotheses you have available to you to prove the subgoal.

Above: proof completed: the day is won… for now.

Finally, Coq introduces complexity by asking you to master only a few basic rules, and then letting you build (and hopefully, eventually solve) bigger and bigger problems from those rules.  A lot of good games do something similar: consider the first half of Portal or pretty much all of Splosion Man.  Those games only obligate you to figure out how a handful of basic mechanics work, but then they’re are able to crank out level after excellent level by gluing those mechanics together, each time in more and more complex and ingenious ways.

Of course, I’m not about to go out on a limb and say that Coq will be the next big game development platform.  For one, their character design has a long way to go (although you have to admit, the ”Proof General” here wouldn’t have looked all that out of place if he’d come on the scene sometime in the mid-90’s):

—Bill