Thank _____ for Static Analysis

Once I talked about why I think static typing (and more generally static analysis) can be really useful, even if I didn't say much. Today I was working on some code and was reminded yet again that, in some cases, without static typing all would be lost, and I would fall into a dark insanity, never to be lucid again.

The code is that of the Tac system, a "framework for implementing and interacting with interactive theorem provers". Originally it was conceived of as a generic tool with which you could develop first an interactive prover for a linear logic, then one for a classical, then another for an intuitionistic logic, all as easy as something relatively... un-difficult. As it stands we have fully developed one such prover, based on the logic µLJ, a first-order logic with (mutually recursive) definitions, induction and coinduction, and generic quantification.

Like Coq, Tac is a tactics and tacticals based prover, in which you manipulate logical sequents by applying tactics (possibly tactics composed of tacticals and tactics) to them. These tactics can be very low-level (a tactic for right conjunction elimination, say), or more complex (a rule for applying some hypotheses to a lemma). In addition, there's a tactic implementing automatic proof search based on focusing which can finds proofs that require nested inductions and coinductions by automatically generating invariants.

To give you an idea of how working with the system might work, here's a proof script showing the process of first defining the natural numbers, defining the even numbers, and then proving that 0 is even (yes, a silly proof) by first unfolding the definition of even, then picking the left branch, and finally recognizing that 0 does in fact equal 0.

#define "nat x := x = 0; sigma y\ x = s y, nat y".
#define "even x := x = 0; sigma y\ x = s s y, even y".

#theorem even_0 "even 0".
mu_r.
left.
eq.

We've also spent a lot of time working on implementing automatic proof search via focusing. Here's a slightly more interesting proof using automation, showing that if x is a natural number then either it is even or its successor is even:

#theorem even_nat "pi x\ nat x => (even x; even (s x))".
prove.

Not an interesting script though.

Anyway, one standard way of implementing such a system is through higher order functions and success and failure continuations (that paper, by Elliott and Pfenning, describes it in the context of logic programming search, but as it is powerful way of implementing backtracking search, it's what we want). The idea is that a tactic is just a function that takes a sequent, a success continuation, and a failure continuation. If application of the tactic on the sequent succeeds, the success continuation is called with the results of the application (more sequents). Otherwise, the failure continuation is called. Tacticals are functions taking possibly several tactics (a list of them, even) and returning a single tactic. Sometimes we have tacticals taking tacticals returning tacticals, and on and on. Lots of useful composable tacticals for doing all kinds of stuff -- the automatic proof search tactical is (more or less) just composed out of simpler tactics.

The point is, after all is said and done, we end up with some fairly complex code. Some of the types defined in the source are third and fouth order, to say nothing of those of the various helper functions whose types are inferred. Working with such complicated code can be pretty hairy, but with O'Caml's type system we've found it relatively easy to work with.

Now, you might say "you're doing it wrong" (I mean come on, fourth order functions?) But let me motivate the design of the system as it stands. First, the tactics and tacticals method of interactive theorem proving has demonstrated its merit in several other systems, so we'll not find a serious case of "doing it wrong" here. Second, the success and failure continuation based approach is, as mentioned, a powerful and elegant way of implementing backtracking search; it's efficient, because all calls are tailcalls, once you wrap your head around the technique it's easy to write new tacticals to compose various tactics correctly, and it cuts the crust off your toast.

Anyway, the point is that while I don't bother about types when writing Python scripts for a MUD I wrote, and I don't even use them to great effect in some of my other projects, sometimes they really are a ____-send.

Postscript 1: fill in the blanks as you see fit.

Postscript 2: Here's an example of the kind of proof that Tac can find; this one is of the fact that "less than or equal to" is transitive. The proof is presented in outlined form, where asynchronous phases are compressed. Click it for a better view.