[FOM] Nelson's proof assistant

[Freek Wiedijk]

Dear Mikhail Katz,

>Unlike his proof, what is certainly not flawed is this excellent illustration
>that computer code can only be as reliable as the programmer, which should
>puncture any "absolute rigor" balloon in case any are still floating.

I'm very much floating the "absolute rigor" balloon.

No, 100% certainty is not possible, for philosophical
reasons.  But 99.9999% or thereabouts certainly is.
I'm not saying we're there yet, maybe not even close,
but I do think it's possible.

I don't think this "qea" thingy was anywhere close to
state of the art proof technology.  I would be very much
surprised if it had the LCF architecture, for example.
In the LCF architecture you only need to trust a small piece
of the program (a couple of hundred lines maybe) for it to
be rigorous.  And one can formally prove the correctness
of that piece of the program too, which has been done in
various approximations for various systems already.

The most interesting project in this direction currently
going on is the verification in Cambridge and Kent of a HOL
kernel together with the ML on which it runs.  Yes, currently
the verification environment still is HOL4 implemented in
PolyML, and the verified environment will be some version
of HOL Light in CakeML, but those two worlds are quite
similar, the gap is closing.  See for details for instance
<http://www.cl.cam.ac.uk/~mom22/itp14.pdf>.

Yes, there's Goedel in the way, and there's a chicken-and-egg
problem here too.  But I do not think that that takes away
that one can get a very high level of rigor this way.

With such a verified LCF-style system, I'd much rather
doubt the consistency of the logical foundations of the
system than the quality of the implementation.  If there
turned out to be a problem, I would wager it would mean we
turned out to have an absolutely rigorous implementation
of an inconsistent foundations.  But if the foundations was
consistent we would have as much "absolute rigor" as would
be philosphically possible.

Freek