[POPLmark] Meta-comment

[James Cheney]

Hi,

On Fri, 2005-05-13 at 12:11 -0400, Robert Harper wrote: 
> As Karl has mentioned, it would be useful, and it seems entirely 
> feasible, to augment the Twelf meta-theorem prover to produce a 
> checkable witness for its inductive proofs.
> 

I think proof terms are only half the answer.  What logic are the proof
terms in, and how do we know that it is sound? (e.g., paper proof?
formal proof? with respect to what mathematical foundation?)

> As to the issue of "trust", I am astonished that there could be any 
> question here at all.  To believe in the consistency of, say, Coq or 
> HOL is an enormous step that requires you to accept strong 
> comprehension principles and that admits no simple inductive 
> characterization to justify them semantically.  In sharp contrast all 
> that the Twelf prover relies on is inductive reasoning over inductively 
> defined sets of natural numbers (ie, the canonical forms of various 
> types, which are easily Goedel-numbered by standard methods).  

<snip>

This is an excellent point, and actually one of the things I really like
about the Twelf approach is that it sticks to elementary techniques
whenever possible (so much so, that it took a while after I left CMU to
understand why people do things any other way).  But you are addressing
a different concern than the one I raised (in fact, one I was trying to
avoid raising).  I will try to restate my concern more concisely.

I was not attempting to argue the merits/trustworthiness of the
foundations of the Twelf meta-logic relative to other possible
foundations, since I am more or less ignorant about this issue (and in
any case, at the end of the day, it's a subjective/philosophical issue,
not a technical one).  My point was that in the absence of a machine-
checked proof of the soundness of Twelf's meta-logic (TML), a TML proof
of phi and a HOL/COQ/whatever proof of phi cannot be regarded as
*formally* (machine-verifiably) proving the same (or comparable) things:

HOL/Coq proof : Foundational theory ======================> phi

vs.

TML proof     : Foundational theory - - - - -> TML =======> phi

where ===> means machine-checked proof and - -> means paper proof.

With the other systems, it is crystal clear what assumptions the system
rests on.  There are many resources I can use to learn about these
foundational systems and decide whether to trust them.  If someone gives
me a proof, I can check/replay it and be confident that the theorem
follows from the axioms of HOL, Coq, or whatever.  All I am being asked
to trust is the foundational theory and the proof checker (both of which
many smart people have thought hard about).

With Twelf, I am not yet sure what the underlying mathematical
foundation for the soundness proof is (e.g., ZFC? ZF? Intuitionistic
type theory + arithmetic?), and while I can easily believe that more
elementary methods suffice, as you assert, to my knowledge the only
evidence is the paper proofs of soundness etc. in Carsten Schuermann's
dissertation (and a few other sources).  Adequacy concerns aside, to
regard a TML proof of phi as a bona fide proof of phi (e.g., in ZFC)
requires one to trust not only a foundational theory and proof checker
but also a large and machine-unverified paper proof.  

This is just the kind of situation we were trying to avoid in the first
place!  How do I know that there isn't a missing lemma, missing case or
non sequitur in these paper proofs?  No criticism of the authors of
these proofs is implied: to err is human.  The highest standard of proof
we have is machine-checked proof, and to my knowledge the extant
evidence of the soundness of Twelf's meta-logic does not meet this
standard.  

Granted, if the Twelf methodology reduces the problem from trusting
paper proofs of many metatheoretic properties to trusting one such
proof, this can be regarded as progress, but the phrase "single point of
failure" springs to mind.

If the soundness of Twelf's meta-logic is straightforward to prove using
elementary methods, it should be no trouble at all to provide a formal,
machine checkable proof, and this (plus proof terms witnessing TML
proofs) would entirely alleviate my concern.  (Of course, a proof using
Twelf's meta-logic itself would not be acceptable, and would probably be
very worrying!). 

I was not arguing that Twelf meta-logic's paper soundness proofs are
*untrustworthy* (at least, no more so than any other paper proof), but
that they shouldn't *have to be* trusted.  In any case, in the absence
of a machine-verifiable proof of this important step in the argument, a
Twelf meta-proof and a development in a foundational system can hardly
be compared apples-to-apples.

--James