[POPLmark] Meta-comment

[Michael Norrish]

Robert Harper writes:
 
> 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).  There is nothing in logic more rock solid than
> mathematical induction.

Andy Pitts gave HOL (universe + rules of inference) a set-theoretic
model in ZFC.  This document is the first section of the Description
manual, available from

  http://prdownloads.sourceforge.net/hol/kananaskis-2-description.pdf?download

> Moreover, the implemented systems mentioned have "features" that go
> beyond even the extraordinarily powerful concepts needed to justify
> the underlying core theories.  If one wishes to be a skeptic, these
> features make the systems even more questionable, not less.

Which features of HOL does the putative skeptic find even more
questionable than ZFC?

Michael.