next up

Episode 1

Imagine you're a machine proving a theorem or perhaps even a person writing a program. What's it like? Well, one approach might be described as synthetic. Basically, you go down the shed at the bottom of the garden and start making the thing. The rest of us don't have any idea what you're doing in there, although we can hear some pretty funny noises. What on earth's making that orange smoke?

Eventually, you emerge from the shed pushing a wheelbarrow containing the proof you have somehow managed to construct. Up the garden path you come to where the typechecker is waiting to inspect your work. I hope you've got it right. If you haven't, you'll just have to go back to the shed and make another one.

The search space consists of complete things, because, whatever you get up to in the shed, that's the only language in which you can communicate with the typechecker. Perhaps, you can take components outside, first little ones, then larger composite ones, leaving us perplexed and intrigued as to what you can possibly be doing.

If you want to explain to how to prove a certain class of theorem, you have little choice but to give a schematic presentation of the proof term in a badly motivated bottom-up way. Of course, this is the traditional style of mathematical writing. It is also the usual way programs are developed. Is there another way? Yes.

Digression: the notes on Propositional Logic from Edinburgh's maths course for first year CS students.