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

[Tjark Weber]

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