[FOM] Formal verification

[Freek Wiedijk]

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