Formal verification of theorems takes a lot of work. And it takes more work where it is least needed. But the good news is that it takes less effort in contexts where it is needed most.
Years of effort have gone into formally verifying the proofs of theorems that no one doubted were correct. For example, a team worked for six years to formally verify the proof of the odd-order theorem in group theory.
Mathematical proofs are fallible, but it’s rare for a proof to be accepted that reaches a wrong conclusion. Flaws in proofs are much more likely to be gaps in reasoning than to be arguments in favor of false statements. And the more people who study a proof, the more likely it is that flaws will be found and fixed.
The return on investment for formal verification is highest for theorems that are the opposite of the odd-order theorem, theorems that are obscure and shallow rather than famous and deep.
For example, suppose you want to prove that a complex set of security protocols doesn’t have any gaps. Your problem is obscure in that only your company cares about it. You don’t have the assurance that would come from thousands of mathematicians around the world reviewing your work.
But on the plus side, your security rules are logically shallow. These rules may be too complicated to hold in your head, but they can be formally specified with far less effort than some mathematical object like a Möbius strip. In general, discrete things like if-then rules are much easier to formalize than continuous things like real numbers.
Mathematicians choose to study things they have some intuition for, and that intuition is often correct even when the reasoning around it is logically incomplete. But businesses are often faced with complex problems they did not chose and problems for which no one has much intuition, such as proving that a complex circuit does what it’s supposed to do, or that an encryption protocol didn’t neglect some edge case. That’s where the ROI on formal methods is greatest.
Oh, wow. Oh, wow.
“…your security rules are logically shallow. These rules may be too complicated to hold in your head, but they can be formally specified with far less effort than some mathematical object like a Möbius strip. In general, discrete things like if-then rules are much easier to formalize than continuous things like real numbers….”
1. For “security” read “business”.
2. If they are too complicated to hold in your head, they are too complicated to explain to a technical writer — or to your successor.
3. “If-then” rules in practice are pinprick bandages for business-logic failures that manifest emergently in production and that are not understood. Legacy business systems consist of decades of accretions like this, most of which have side effects.
3a. You neglect the ever-popular “dangling else”.
“RIO on formal methods is greatest” should probably say ROI, not RIO. Unless you actually meant to laud the skills of Brazilian mathematicians. :-)
I don’t think it’s rare for “false theorems” to be accepted. Quite often one sees statements of theorems being (pedantically) incorrect, because eg some “obvious” hypothesis is omitted, like such and such a rational being non-zero.
If you want to know exactly what’s been proved, look at the proof.