next up prev

Episode 2

Now imagine we're inside the shed. Our task is, let us say, to make some kind of monument. So far, we've found a plinth with a round hole into which we've put a pedestal. This leaves us with a square hole waiting to be filled. Before, we try to finish the work, perhaps with that statue, can we be sure we have not already gone wrong? If only we could ask the typechecker.

If we had a typechecker who understood things with holes in, we could build them in a top-down fashion, checking them whenever we like. In particular, we can ask him to confirm that each move we make is acceptable, so that when we eventually wheel the finished work of art up the garden path in the wheelbarrow, we know it will meet with approval.

This is the way proof assistants work. However, in LEGO, the treatment of holes is not entirely reliable. That's not the typechecker, you see... That's the typechecker's evil twin! Sometimes he lies and accepts steps he should forbid, and when we wheel the proof outside, the real typechecker says no.

So what do we need?