[FOM] Formal verification
Freek Wiedijk
freek at cs.ru.nl
Tue Oct 21 15:14:57 EDT 2014
Dear Arnold,
>Whereas making a mathematically fully acceptable proof written in
>Latex formally rigorous (i.e., acceptable to a proof assistent) has
>an overhead factor of roughly 40, and currently returns nothing but
>an increases assurance of correctness.
I always claim that properly formalizing a textbook page
is about one week of work without doing much else. So you
claim you could write and polish a latex page in a single
workhour then? Well, maybe.
And formalization is not just about correctness, it's
also about _explicitness._ With a formal version of math,
there is no space for unclarity what the definitions and
steps in the proofs are. I think that was Lamport's point
in his How to Write a Proof.
Freek
More information about the FOM
mailing list