[FOM] Solution (?) to Mathematical Certainty Problem

[Roger Bishop Jones]

On Saturday 21 June 2003  6:04 am, Harvey Friedman wrote:

<snip>

> We now come to the novel(?) idea here.
>
> The idea is that so much information in the form of pointers,
> etcetera, into the proof in T is given after the end of the
> proof in T, that this alleviates the need for parsers, string
> searchers, and the like in the core proof checker. (We have
> not yet come to the core proof checker).

<snip>

> Extreme annotation will be so explicit that the core proof
> checker has only to do completely trivial grunt work of the
> most elemental kind.
>
> We think that one should be able to easily program the core
> proof checker in an appropriate MACHINE LANGUAGE, and have a
> mathematician write a completely readable correctness proof of
> the machine language program that is completely convincing to
> any mathematician. Special purpose hardware would circumvent a
> number of verification issues.

The idea that machine verification can and should be organised
in such a way as to make the core proof checker a very simple
program is by no means new.

There are at least two well-known paradigms for verification
which are based on this idea.

The most famous and widely used is the "LCF paradigm",
which originates in the proof assistant for Dana Scott's
Logic for Computable Functions (LCF) which was developed
at the University of Edinburgh in the 70s (i.e. about
30 years ago), by a team lead by Robin Milner. 

In this method the key code critical to
proof checking is separated out into a small logical
kernel and the more elaborate programming which supports
user interfaces or sophisticated proof search algorithms
is thereby rendered incapable of making mistakes which
go undetected.

As well as establishing an architecture for reliable proof
verfication, this research invented a new functional programming
language for developing proof checkers, which was called
"ML" (for meta-language).  Descendents of this language
are used to this day in the programming of many proof assistants,
which when implemented in these languages usually follow
the LCF paradigm.  Among the many such tools are:

	HOL (a tool for Higher Order Logic)
	ISABELLE (A generic proof system)
	COQ (for Coquands calculus of constructions)
	NUPRL (constructive type theory)

A second well documented method of maximising the assurance
with which proofs can be checked is that mandated by
UK Defence Standard 00-55 for use in the development of
safety critical military software.
This involves the use of verification software which
is capable of exporting a primitive proof script
for verification by an independent proof checker.
Such a proof checker is envisaged as being simple
enough to be itself readily verifiable.

I am myself less familiar with the application of this
method, but I believe there are  proof tools which have
the capability to export proofs for this purpose.

On a brief perusal, the least credible aspect of your
proposal is that your language T (and other aspects
of your proposal) should become a universal standard
adhered to thoughout the world.

There is not the least chance that this could happen,
nor should it!

Roger Jones