[POPLmark] Re: Meta-comment

[John R Harrison]

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

For HOL at least, hyperbolic adjectives hardly seem merited. The logic
might be strong compared with PRA, but most mathematicians assume, at
least implicitly, the consistency of significantly stronger systems like
ZFC. To me, a more pressing concern is whether the actual code for the
system implements the well-understood logic correctly.

A few months back I tried a little experiment of formalizing a semantics
for HOL without the axiom of infinity inside HOL Light itself, and
proving the correctness with respect to that semantics of an idealized
version of the HOL Light core code. This can be seen as an attempt to
tackle both issues at once: formalizing the logic itself and the
particular implementation details. As yet, HOL's definitional extension
principles are not covered, and neither are all the OCaml features used
in the code (e.g. optimizing away term rebuilding by checking pointer
equality). Still the approximation is at least close enough to make me
pretty happy that there are no more variable renaming bugs.

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

What are the features you're talking about here?

John.