[FOM] FOM comment

[Bob Constable]

The mail from Prof. Paulson was very interesting, especially the
following comment on how we know that proof assistants are
correct.

============
HOW CAN WE DESIGN THE ULTIMATE VERIFIER IN ORDER TO BE BEST SUBJECT TO VERIFICATION?

In recent years, there has been much promising research in the use of proof assistants (especially HOL Light and HOL4)
to verify their own kernels, and even to verify their translation into machine code. This is as high as standard as one
could wish for. On the other hand, if we are demanding that these systems should be verified, it seems perverse to trust
them for their own verification. Therefore we need the proofs to human-legible as well. They aren’t at all just now. But as
somebody who uses such systems almost daily, I’d like to remark that confidence in such a system can be confirmed by its
stubborn refusal to prove something in the presence of even the tiniest error in the set up.

Larry Paulson
============ =====================================
Here are some closely related results recently published.

Two Cornell researchers, Abhishek Anand and Vincent Rahli, launched a project to
prove correctness of the rules for Constructive Type Theory (CTT) implemented by
the Nuprl proof assistant. They formalized Allen's per semantics for this theory in the
Coq type theory and proved in Coq over a hundred rules correct.  Here is a pointer to
their technical report and article.  All of this and related work is available at the
PRL project page:  www.nuprl.org.

===
Towards a Formally Verified Proof Assistant
http://www.nuprl.org/KB/show.php?ID=726

Abstract
This paper presents a formalization of Nuprl's metatheory in Coq. It includes a nominal-style definition
of the Nuprl language, its reduction rules, a coinductive computational equivalence, and a Curry-style
type system where a type is defined as a Partial Equivalence Relation (PER) à la Allen. This type system
includes Martin-Löf dependent types, a hierarchy of universes, inductive types and partial types. We then
prove that the typehood rules of Nuprl are valid w.r.t. this PER semantics and hence reduce Nuprl's
consistency to Coq's consistency.

==================

Recently this formal Coq model of CTT was used to validate mechanisms that allowed
Mark Bickford and Vincent Rahli to prove an important instance of Brouwer's
Continuity Principle for use in CTT.

A Nominal Exploration of Intuitionism
http://www.nuprl.org/KB/show.php?ID=749

Abstract
This papers extends the Nuprl proof assistant (a system representative of the class of extensional type theories
à la Martin-Löf) with named exceptions and handlers, as well as a nominal fresh operator. Using these new features,
we prove a version of Brouwer's Continuity Principle for numbers. We also provide a simpler proof of a weaker version
of this principle that only uses diverging terms. We prove these two principles in Nuprl's meta-theory using our formalization
of Nuprl in Coq and show how we can reflect these metatheoretical results in the Nuprl theory as derivation rules.
We also show that these additions preserve Nuprl's key meta-theoretical properties, in particular consistency and the
congruence of Howe's computational equivalence relation. Using continuity and the fan theorem we prove important
results of Intuitionistic Mathematics: Brouwer's continuity theorem and bar induction on monotone bars.