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.