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

Tjark Weber tjark.weber at gmx.de
Thu Oct 23 11:27:28 EDT 2014


On Wed, 2014-10-22 at 15:13 -0400, Dustin Wehr wrote:
> You aren't being naive at all. The problem is the Interactive Theorem
> Proving community's obsession with "trusted small kernels".

I don't think there is such an obsession (but perhaps a healthy focus).
Trusted small kernels are motivated by the very practical engineering
challenge of developing a sound theorem prover.

> They are not interested in conditional verification. If you write the
> kind of computer-checkable formal proof that I think you have in mind,
> where you take as assumptions theorems/lemmas that are routinely proved
> in undergraduate math classes, it will be regarded as incomplete and
> ignored. They aren't satisfied until everything is encoded/defined
> using inductive datatypes, sets, provably-halting programs, etc.

There is plenty support for conditional verification in today's
interactive theorem provers. For instance, you can easily defer the
proof of a lemma, or work within a context of unproven assumptions
(axioms).

However, unproven assumptions are a common source of error. Time and
again, some "obviously true" lemma that is assumed (rather than proved)
fails to hold. Hence, there is healthy skepticism towards unproven
assumptions.

Best,
Tjark




More information about the FOM mailing list