[FOM] response to Lasse Rempe-Gillen (Re: Formal verification)

[Freek Wiedijk]

Dear Dustin,

>The problem is the Interactive Theorem Proving community's
>obsession with "trusted small kernels".

Certainly not.  Only the HOL based systems have that.
Coq claims to have that, but the Coq kernel is a large piece
of code (written by very clever people, and very interesting,
but _not_ small).  And systems like Mizar, PVS, ACL2,
the B method, etc. they all have no small kernels at all.

>They are not interested in conditional verification.

That's a totally different thing.  Mizar, PVS, ACL2, the
B method, etc. are not about conditional verification,
that's right.

Conditional verification has been proposed many times,
as "really needed to make progress".  For example it's
the basic philosophy of Theorema's "proof exploration",
and I remember Peter Aczel making a strong point for it.

The problem is that when you don't formally prove everything
you use, the probability that what you write down will be
wrong is very high.  Take that example were the continuity
of f was forgotten to be stated.  As we know from software
_all_ programs have bugs.  That same phenomenon will rule
when using this approach as well.  There won't be formal
correctness.  It's not about doing uninteresting work,
it's about getting everything right.

Now if you don't mind that the "conditional verification"
thing might be for you.  But I like my math correct :-)

With this attitude, you get systems like this "qea" thing,
I think.  It sounds like it's about formal math, but you
don't really get something you can trust.

Freek