[FOM] mechanical theorem metachecking

[hendrik@topoi.pooq.com]

I've been wondering about the possibility of mechanical theorem
metachecking.

Let's say we have a formal system F.

In F, we prove that the execution of some computer program P(x) will,
if it terminates, always generate a formula that is provable in F.

Since execution of P on a machine may be more efficient than
checking the proof it generates, we're tempted to include a rule
that allows us to use such proved programs as proof rules in F.

Under what circumstances is it possible to do this safely?

If it is impossible as stated, what variations on the question could 
yield safe proof-checking?

-- hendrik