[POPLmark] Meta-comment

[Karl Crary]

James, the same picture must be drawn for any system; all that differs 
is the subjective judgement of the length of the arrows.  The calculus 
of constructions, for instance, relies on a sophisticated normalization 
result using reduction candidates, and that's even before you add 
inductive types.  If you compare Werner's thesis to Schuermann's, I 
think you'll be hard-pressed to draw Twelf's arrow much longer than Coq's.

Then there's the question of the strength of the original foundation, 
which ought not be ignored.  If I'm not mistaken, Twelf's soundness can 
be justified in terms of first-order Peano arithmetic (which, as Bob 
noted, is the most solid foundation there is).  HOL most certainly 
cannot.  I'm not sure about Coq; perhaps someone more knowledgeable in 
these matters can enlighten me.

    -- Karl


James Cheney wrote:

>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
>
>_______________________________________________
>Poplmark mailing list
>Poplmark at lists.seas.upenn.edu
>http://lists.seas.upenn.edu/mailman/listinfo/poplmark
>
>
>  
>