[POPLmark] Meta-comment

[Frank Pfenning]

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

I agree it is unfortunate that the theory of M2, the current meta-logic
in the Twelf system, has not been formalized.  And I grant that its
trusted computing base could and should be smaller.  However, I think
you are idealizing the other systems.

I may be wrong about each of those---if there is someone listening
who has better knowledge, please correct me.

- Isabelle/HOL uses type variables, type classes, and overloading.
  I believe there is an argument for the correctness of this (a note
  by John Harrison?), but it is certainly different from pure
  Church's type theory (often called Higher-Order Logic).
  Also, I don't believe that the theory of higher-order logic
  in the presence of description and/or choice operators is
  really all that well understood.  Chad Brown's recent thesis
  makes a lot of progress in understanding extensionality and
  equality, but description is still outside its scope.

- Last year, Kevin Watkins discovered a bug in the substitution
  algorithm in the trusted core of HOL-light due to a problem
  with alpha-conversion.  I believe this bug had no consequences
  for the standard libraries.

- The Calculus of Inductive Constructions (CiC) is rather complicated
  by itself, and few people would claim to understand its theory fully.
  In addition, the Coq implementation has a module system
  which, I believe, is not conservative over CiC.  While Courant
  has investigated its theory, I think it is far from crystal
  clear exactly what assumptions it rests on.

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.

  - Frank