[FOM] formal proofs

[Till Mossakowski]

Am 14.10.2014 03:24, schrieb Harvey Friedman:
> 1. Exactly why and exactly in what sense should be trust this kind of
> "absolute rigor"? Since the answer is certainly at least "in several
> really good and interesting senses", one should raise the bar for an
> answer to this question very very high. How high can be bar actually
> be raised? Another way of talking about this is perhaps the
> recognition that there has to be some "core" human involvement that is
> "absolutely accepted to be absolutely obvious". But what should such a
> "core" consist of? What kind of obviousness is involved? Can this
> "core" be simplified? Can this "core" be ultimately simplified, so it
> cannot be simplified further? And does all this mean - say, what does
> all this mean, rigorously? I.e., where is the general theory of
> "cores"?
>
There is the LCF-style architecture used by some theorem provers, e.g.
Isabelle.
It entails that the type system of the programming language (typically
ML) ensures that proofs can only be constructed by a small trusted
code-base (typically some few hundred or thousand lines). The
obviousness involved is that for more than a decade, no flaw has been
found in the Isabelle trusted code-base (and neither in the
implementation of the ML type system, which of course has to be trusted
as well).

See e.g.
http://events.inf.ed.ac.uk/Milner2012/slides/Paulson/LCF+-without-transitions.pdf
or chapter 8 of "Mechanizing Proof: Computing, Risk, and Trust" by MacKenzie

Then, there are also verified theorem provers, but as far as I know,
only experimental versions, e.g.
http://link.springer.com/chapter/10.1007%2F11541868_19
In the future, this could be used for a kind of bootstrap procedure,
where a prover like Isabelle is used to verify its own trusted code-base.

Till Mossakowski