[FOM] Mathematical Certainty?

[Roger Bishop Jones]

Probably the most ambitious "practical" approach
to realising near-absolute certainty in demonstrating
mathematical propositions was the "CLINC stack".

This was a project conceived by the now defunct
Computation Logic Inc (CLINC) to build a stack of
verified components.

i.e. a verified microprocessor running verified
operating system, language compilers and theorem
provers.

Computational Logic was a company formed by
    * Robert S. Boyer
    * Richard M. Cohen
    * Donald I. Good
    * J Strother Moore
    * Michael K. Smith 

I think originally based around the "Boyer-Moore"
theorem prover developed by Boyer and Moore
and the Gypsie program verification system of
Don Good.

CLINC was particularly strong in hardware verification
and Warren Hunt at CLINC accomplished the first complete
formal verification of a microprocessor.

This was largely funded by the US government during a
period (long ago) in which mathematical proofs were thought
to be an important way of realising more secure computer
systems.

CLINC => http://www.cli.com/corp/research.html

A more recent attempt at something similar was the
EU funded PROCOS project.
http://www.afm.sbu.ac.uk/procos/

I would have thought that for FOM more theoretical or
philosophical lines of investigation are more interesting.
In particular:

(1) The problem of regress in the foundations of semantics.
and
(2) How to achieve maximum confidence that formal systems
    are sound with respect to their semantics.

Of course, to address these, particularly (1), you need
to recognise that there is some uncertainty about what
(e.g.) set theory _means_, and be interested in saying something
more informative than that set theory is "about sets".

Roger Jones