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

[Dustin Wehr]

Freek, Till, Tjark, Andrei,

Thank you for your thoughtful responses to my (admittedly
over-spirited) message. Freek, thank you for reminding me of Theorema;
I should have mentioned it. I thought that project had been
effectively abandoned for years, but I see they released version 2.0
just a few months ago. I should have also mentioned William Farmer's
IMPS (appears abandoned) and the "little theories" approach he
advocated, which is basically what I was talking about. I was being
careless when I wrote "trusted small kernels"; I really just meant
what Farmer called the "big theories" approach, i.e. that all the
developments are conservative extensions of some base theory.

I think for building libraries of formalized mathematics, which will
be used by others without their personal scrutiny, the popular ITP
systems are doing things right. But how useful are they for a
mathematician who simply wants to formalize one of their recent
proofs, who doesn't want to have to spend weeks (months?) learning to
use an ITP system efficiently? Such a person is ok with the
possibility of their proof containing errors, since they are already
publishing proofs in natural language. And if a system was designed
specifically for that kind of conditional proofs work, then errors
would be _so much easier to find_ than in natural language proofs. Is
Theorema such a system?

Finally, can I plead that we not say that "_all_ programs have bugs"?
Of course it is intentional hyperbole, but I think even with that
proviso it's misleading. There are many, many completely-correct
programs that will never have formal proofs of correctness. The truth
is that we learn to program carelessly. I suspect it's because
programming is more fun that way, and because often the cost of errors
is not that high (especially considering the likelihood that the
program will be abandoned in the future, due to changing
specifications or moving to a different software framework). Even in
the small amount of work I've done writing formal proofs, I have
introduced inconsistencies, but I, like Lasse in his earlier message,
was certainly not being careful.

-Dustin