Subject: Re: dealing with errors (was: "Programming is FUN again") From: Erik Naggum <clerik@naggum.no> Date: 1998/03/29 Newsgroups: comp.lang.lisp Message-ID: <3100169086878095@naggum.no> * Rob Warnock | Not as "precise", but certainly as "correct", yes? You won't deny, I | hope, that incorrect specifications usually lead to incorrect functioning | of the total system, *especially* when the code is proven to implement | the specification! no, I won't deny that, but there is an important difference between what constitutes a correct program and a correct specification: the latter must not contain inconsistencies or conflicts. a program must be allowed to contain inconsistencies and conflicts because it is impossible to do everything at once. since a specification is a statement of the static properties of a program, and a program's execution is a dynamic process, the types of incorrectness that can occur are vastly different in nature. this all leads to simpler (to express and implement, anyway) requirements on specifications than on programs. since the program should now be derived from the specification, we have removed a tremendous fraction of the randomness in the way humans think and process information. writing specifications, however, is much harder than writing programs, but at least you can always know whether it is internally consistent or not. | The problem I was noting in that postscript was that in attempting to | prove *total system* correctness [as opposed to proving correctness of an | encapsulated library component, which is often fairly straightforward] | one eventually must regress (step back) to the initial human desires that | led to the specification -- whereupon one runs smack bad into the | "DWIS/DWIM" problem ("Don't do what I *said*, do what I *meant*!"), which | at its root contains the conundrum that much of the time we humans don't | actually *know* exactly what we want! oh, yes. total system correctness is often meaningless even if it can be proven just for this reason. I see that we don't disagree on much, but I have become wary of the many paople who argue against proving correctness of components because of the human factors in "satisfiability" overshadow any correctness properties of a system at some point close to the users. | We violently agree. However, I was trying to warn that that *still* | isn't enough to prevent disasters, since the best you'll ever get with | the best methodologies is code whose behavior meets the originally stated | goals... WHICH MAY HAVE BEEN WRONG. we violently agree, indeed. | Yet I think we also agree that the truth of this point is no excuse | for not using the best methodologies we have access to *anyway*... precisely, and to wrap this up: I think the report from the Ariane 5 failure was incredibly intelligent and honest about the issues they were involved in. would that similar efforts would be undertaken when software less critical also fails. there is a lot to learn from mistakes that we probably never will learn from until we get rid of the obvious mistakes that we _believe_ we know how to handle. I'm reminded of a "definition" of insanity that might apply to programming: to keep doing the same thing over and over while expecting different results. the irony of this whole verifiable programming situation is that we are moving towards the point where we can prove that human beings should not write software to begin with, and we let computers program computers. however, as long as C++ and similar repeatedly-unlearned-from mistakes hang around, programmers will still be highly paid and disasters will come as certainly as sunrise. #:Erik -- religious cult update in light of new scientific discoveries: "when we cannot go to the comet, the comet must come to us."