[FOM] Mathematical Certainty?
Roger Bishop Jones
rbj at rbjones.com
Sat Jun 21 02:31:02 EDT 2003
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
i.e. a verified microprocessor running verified
operating system, language compilers and theorem
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
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
CLINC => http://www.cli.com/corp/research.html
A more recent attempt at something similar was the
EU funded PROCOS project.
I would have thought that for FOM more theoretical or
philosophical lines of investigation are more interesting.
(1) The problem of regress in the foundations of semantics.
(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".
More information about the FOM