[FOM] Formal verification

[Andrei Popescu]

Hi Dustin, 

Dustin Wehr wrote: 
>> The problem is the Interactive Theorem
>> Proving community's obsession with "trusted small kernels". 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

A main reason why this community is so harsh on axiomatizations that could be replaced by definitions and proved theorems is the following: a prover's automation could take advantage of the tiniest inconsistency (e.g., the name of a variable spelled wrongly) to derive very wild things, within a butterfly effect: you axiomatize "textbook" fact A (and get it slightly wrong), then you infer from it a "well-known but nontrivial" fact B (and also get this slightly wrong, but can prove it nevertheless using the faulty A), then you move to conjecture C which will follow easier than you expect.  :-)  You may argue that such silly errors would eventually be discovered, but perhaps the *cheapest* way to discover them is try to prove the provable and keep the kernel small.    

All the best, 
  Andrei