Is Verification Necessary

Let this page be conducted in accord with the SummaWay of debate, as an experiment. The disputed question is:

First Article. Whether formal program verification is necessary?

Objection 1. It seems formal verification is not necessary, for it is impossible to verify any non-trivial program, and it has been said "all nontrivial programs have bugs". What cannot be done, cannot be mandated. Therefore, program verification is not necessary, and testing, sufficient.

Objection 2. Furthermore, to be necessary, a procedure must meet some requirement not otherwise attainable. But SusanJohnson, of many years experience making pace makers, says in ExtremeProgrammingChallengeThree I've never seen a proof of correctness, and our products work just fine, thank you. Therefore, verification is not necessary.

Objection 3. Furthermore, even if a program can be proved correct, the compiler, virtual machine, libraries, processor, peripherals, and so forth must also be proved correct to completely certain, which is impractical.

Objection 4. Furthermore, 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 methodologists.

Objection 5. ?

On the contrary, Fred Brooks in MythicalManMonth writes "Program verification is a very powerful concept, and it will be very important for such things as secure operating systems. The technology does not promise to save labor, though".

We answer that, formal program verification is necessary if the probability and consequences of failure are immediately life-threatening. Conversely, if failure is life threatening, and it cannot be verified, it should not be built.

Reply Objection 1. DavidParnas quoted in ParnasSoftwareReviewPatterns reports success using a review method, based on reconciling the formal specification of a system with a formal description of the system as implemented

Reply Objection 2. DaveHarris shows An admirable past safety record does not guarantee a safe future when he argues Testing only covers a finite, and usually small, number of cases. The number of cases in the wild is unbounded and usually large. Therefore, testing cannot do an adequate job. You need a static analysis which can cover infinitely many cases, otherwise you are never quite sure.

Reply Objection 3. AlistairCockburn notes Verification can be necessary without being sufficient

Reply Objection 4. Nor can there be any experimental evidence there are an infinity of PrimeNumbers?. The objection presupposes what cannot be known by experimental method, cannot by known by other rational means.

Reply Objection 5. ?

yea x AlanWostenberg, ... nay x ...

The Summa is a summary of, not a structure for, live debate. This debate has some history, which I extracted. I've also defended my own position as you see above. As the rough raw debate carries on here below the line or onto other pages, I'll excerpt new objections and defenses above the line. So, any further objections or replies? --AlanWostenberg

Struggling with the format, not of the given arguments, but of how I am allowed to add / modify. I feel the format biases toward objections. I also think "verification" is still ambiguous, as given in Object 3 and Object 3 Reply, below. Finally, if I sign on Yea, does that mean I answer Yes to the proposal at the top? -- AlistairCockburn

Objection 1 Reply. ...program verification is not necessary, and testing, sufficient. ExtremeProgrammingChallengeFourteen provides a counterexample, as do the problems of synchronization and mutual exclusion taken up by LeslieLamport?.

p.s. May I make a motion to amend the proposal to read: Whether formal program verification can be necessary, even if not sufficient? See IsProofNecessaryNotSufficient?

See Tom's proposal next -- AlanWostenberg

The We answer that section needs some buffing up. How, for example, can the probability of failure be life-threatening? Have "formal program verification" and "to verify" been defined, and does the latter imply the former? If this section were repeated as an objection in another's article, it would be simple to reply to it.

Further, "Whether formal program verification is necessary" is the first article, but what is the question? (A "question," in the SummaWay, is composed of several articles, all of which relate to a common idea.) Perhaps the question is something like Verification, and the first article should be something like "Whether formal program verification is possible," followed by "...necessary," then "...sufficient."

Finally, a Summa DesignPattern is MakeDistinctions?. Often the objections are perfectly valid, but do not apply to the particular question as interpreted by the author. So, for example, the claim that "our products work just fine" might be shown to be an answer to a question distinct from that posed by verification. Distinctions need to be drawn between verification, testing, and whatever else might be considered. -- TomKreitzberg

Yes. In Wiki the broad question could be OnVerification?, with the three articles IsVerificationPossible?, IsVerificationNecessary, IsVerificationSufficient?. -- AlanWostenberg

The question is either a strawman or needs more explanation.

Verification is clearly not necessary because almost no successful programs are verified. I've never heard any of its proponents say it is NECESSARY. They just say it is a good idea, will pay for itself in some projects, will make programs more reliable than with other techniques, etc. My personal opinion is that verification of entire programs is very rarely a good idea, though verification of small parts of programs is sometimes a good idea. But this question seems to me to be unfair to those who like verification because it grossly overstates their position. They don't say it is necessary, they just say it is a good idea. -- RalphJohnson

Necessary for what? I agree that verification is clearly not necessary to build useful software. However, to find out whether this piece of software can be subverted by a buffer overflow attack, simple testing isn't enough. It seems to me that sort of (possibly informal) verification is necessary to find out whether this piece of software can be subverted by a buffer overflow attack. -- DavidCary.

As it turns out, this is really not a simple yes/no article, I need to restate it as a broader question with several related subordinate yes/no articles, as Tom suggested. Even so, "is it sometimes a good idea" is not a crisp yes/no question, so we'd have to tighten that up. -- AlanWostenberg