[FOM] Talk on Formal Verification

[Mario Carneiro]

On Wed, Feb 3, 2016 at 9:32 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:

> > Of course, ifyour community actually does certify something that later
> turns out to be flawed, and top researchers were involved, then that is a
> whole new story. I assume that that hasn't happened, at least for a
> longtime?
>
> As far as I’m aware, nobody has ever published a machine proof of a
> theorem that turned out to be false. A number of software errors have been
> reported in various systems, and it’s encouraging that generally these have
> been recognised by the users themselves.
>

Usually, a bug in a proving software is demonstrated to be an actual bug by
proving a contradiction. Since contradiction "turns out to be false",
doesn't this trivially satisfy the requirement, and make bugs in a prover
more or less synonymous with false formal proofs?

Taking the question less literally, I don't think there are any examples of
major results that were subtly flawed as a result of a bug, without simply
passing via the principle of explosion.

Mario
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160203/e4093093/attachment.html>