[POPLmark] Meta-comment

[James Cheney]

Hi Frank and Karl,

On Mon, 2005-05-16 at 11:57 -0400, Frank Pfenning wrote:
> [James Cheney wrote]
> > With the other systems, it is crystal clear what assumptions the system
> > rests on.  
<snip>

> Don't get me wrong---I have the greatest respect for the developers of
> these systems and I believe they are well-engineered and rest on good
> foundations, but I don't see that their basis is crystal clear or in
> some essential way better understood than Twelf.

Where I wrote "it is crystal clear what assumptions the system rests
on", what I meant was "the axioms/inference rules constituting the
system are clearly spelled out" (and, everything past that point is
machine checked).  Your points (like Bob Harper's earlier remark) appear
to address a different claim that I did not make (and wouldn't try to
defend), namely, "the full implications of the axioms and rules
constituting the system are crystal clear".

On Mon, 2005-05-16 at 11:03 -0400, Karl Crary wrote:

> 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.

My feeling is that arguing mathematical foundations is, like arguing
religion, text editors, operating systems, or programming language
preferences, basically a subjective issue which we can debate all day
and not get anywhere.  While this is certainly an interesting and
relevant discussion to have in this context, it's one I lack the
expertise to contribute to.  

I am happy to concede the point that Twelf meta-reasoning can (probably)
be justified using a simpler mathematical foundation than for other
systems, and that if so, this is an advantage.  It is the strength of
the evidence for this claim (that is, whether "probably" can be removed
from the previous sentence) that I am trying to ascertain.  I don't
think my earlier messages were ambiguous about this concern, but it may
have got lost in the noise, so I will rephrase it.  I apologize if am
being obtuse or excessively verbose/pedantic.

I regard a (carefully written and reviewed) paper proof as only "beyond
a reasonable doubt" (i.e., a high, but not the highest standard of
evidence) and machine checked proof as "beyond a shadow of a doubt"; it
is this highest possible standard to which we aspire.

I believe that extant paper proofs provide "beyond a reasonable doubt"
justification for Twelf's soundness.  The point I have been trying to
stress here is that this evidence does not yet appear to meet the
"beyond a shadow of a doubt" standard of machine-checked proof.  This
seems like a crucial link in the argument that Twelf proofs are bona
fide formal proofs of what we intuitively want to prove.

In contrast, a completely formalized proof in an LCF-style system (Coq,
HOL, etc) is held to the higher standard "beyond a shadow of a doubt"
throughout the development. It is possible that I am idealizing these
systems or being unfair to Twelf, but I think that the designers of the
LCF-style systems would agree that while the systems may not have the
above property yet, it is a central design goal.  If your point is that
this is the case for Twelf also, OK, but it seems to me that the other
systems are closer to realizing this.  Perhaps this is subjective too
(and perhaps there are important not-yet-formalized parts of the other
systems that I'm not aware of).

This means, to me, that the approaches are not strictly comparable in a
technical sense: Twelf proofs rely on soundness and adequacy theorems
that are apparently not completely machine checked (and probably could
be), and (not coincidentally) proofs are often easier to develop using
Twelf.  On the other hand, proofs in LCF-style systems are machine-
checked from first principles, and (not coincidentally) appear to
require more effort to develop.  Thus, I think there is room for
improvement in both classes of techniques: in the former by establishing
soundness beyond a shadow of a doubt, and in the latter by improving
automation for "typical programming language reasoning" to the high
level attained by Twelf.  

In any case, I'm starting to get the feeling that I'm guilty of not
letting ignorance deter me from having strong opinions, so I'm happy to
admit that perhaps

1.  I'm asking for an unrealistically high standard of evidence, or
2.  I should stop splitting hairs and do some real work, or
3.  I'm being unnecessarily disagreeable, or
4.  I should read more papers/theses.

and leave it at that.

--James