[FOM] Machine-checkable proofs: NP, or worse?

[Timothy Y. Chow]

I've been having an email discussion with Tjark Weber, who has almost, but 
not quite, convinced me that proofs that take a feasible amount of time to 
check but whose certificates take an infeasible amount of space to write 
down do not pose a problem.

The general idea is that one creates a runtime environment in which 
theorem objects can be created only by a small set of trusted 
"verification" routines.  One can then create a complex piece of code 
that, for example, systematically searches the checkers game tree, and 
repeatedly calls the verification routines to create theorem objects on 
the fly.  The proof certificate never has to be stored all at once in 
memory or on disk anywhere.  At the same time, if the complex piece of 
code has bugs in it then all that can happen is that the desired theorem 
objects won't get generated because the verifier subroutines won't be 
convinced.  Only the verifier needs to be bug-free.

What bothers me about this scenario is the question of how one ensures 
that the theorem objects cannot be created except by the verifier.  After 
all, what we are executing is the complex piece of code; we're not 
executing the verifier directly (with a certificate as input).  Can we be 
sure that the complex piece of code isn't maliciously exploiting a subtle 
bug in the operating system to generate unauthorized theorem objects?

Probably with the right security measures in place, this kind of problem 
can be addressed.  It seems like a subtle business to me, though.

Tim