Is Proof Necessary Not Sufficient

Trying to keep this page summarized in a variation of SummaWay, to see whether the argumentation has less back-and-forth. Slightly different question from IsVerificationNecessary.

Matter. Whether formal proof of program design can be necessary (even if not sufficient)?

Con 1. Formal proof is not necessary, for it is not possible. It is impossible to prove any non-trivial program.

Con 2. Formal proof is not necessary, because testing is sufficient. There is little or no experimental evidence that shows verification to be better than testing, or for that matter, better than nothing at all. While verifiers report good results, so do testers and so do reviewers and so do all sorts of methdologists. Failure of all other techniques does not prove the efficacy of verification.

Con 3. Formal proof is not necessary, because it does not actually guarantee anything. Even if a program's paper design were to be proved correct, the compiler, virtual machine, libraries, processor, periferals, and so forth can introduce defects, unless they are also proved correct (which they can't, due to Con 1 and Con 3 at a lower level of implementation). The problem explodes when it comes into contact with the rest of the world.

Con 4. Formal proof is not necessary, because proof is capable of being checked only by human inspection. Thus, a formal proof is more likely to be incorrect than the program it allegedly describes.

Con 5. Formal proof is not necessary, because proof, if correct, only applies to the program as (believed to be) originally written. Most programs require change. Proofs would need to be updated with every change. This is unlikely to occur.

Con 6. Formal proof is not necessary, because only a tiny proportion of these critical programs have in fact been proven, yet the world has not suffered serious effects. Thus, the probability of critical failures is sufficiently low without proof.

Pro 1. There are problems that are so tricky that unless the design is rigorous proved, no amount of coding and testing will adequately demonstrate correctness. Reference LeslieLamport? and PerBrinkHansen?'s work on mutual exclusion and serialization.

Pro 2. There are systems whose consequences are so far reaching that unless there is rigorous proof of key sections, the damage that can accrue is simply too devastating to consider. Atomic power plants and pacemakers would be two such systems. Such systems should not be built if their core design cannot be proved.

Con 1 Replied: Con 1 is an argument for sufficiency, not necessity. If a proof is necessary only for one section of one program, then it is necessary (and perhaps not sufficient). And it is possible to prove the core element of the design. The HDLC protocol has been proven correct, as have certain distributed algorithms. The Cleanroom methodology prescribes a hierarchical proof system and coding rules that have been used on very large systems.

Con 2 Replied: Formal proof of such systems is necessary because testing is insufficient. It is well known how often defects occur in software, particularly complex or distributed systems.

Con 3 Replied: Formal proof is necessary and also not sufficient, just as testing is necessary and not sufficient. If the basic design is not correct, testing cannot be guaranteed to show the flaw. Yet, even if the design is proved correct, certain mistakes may still creep in through an implementation flaw somewhere down the line.

Con 4 Replied: Formal proofs can be checked automatically. For example, see the CoqProofAssistant.

Con 5 Replied: Proofs and programs are developped in tandem. Unless the (automatic) theorem checker succeeds in checking the proof, no executable is generated.

Pro 1 Replied: Reference XpChallengePaceMakers, where SusanJohnson said, of many years experience making pace makers, ''I've never seen a proof of correctness, and our products work just fine, thank you."

Pro 2 Replied: None of them have been proved correct.

Pro x AlanWostenberg, AlistairCockburn ... Con x RonJeffries (quelle surprise)...

To add your view, strengthen either the basis or the reply for your view.

This format reads rather like a modern brainstorming session transcript.

It seems there are enough pros/cons here indicating this is not a simple yes/no article, that it is complex enough to warrant a general question, grouping related simple articles, as Tom K suggested over in IsVerificationNecessary.

--AlanWostenberg