Subject: Re: dealing with errors (was: "Programming is FUN again") From: Erik Naggum <email@example.com> Date: 1998/03/28 Newsgroups: comp.lang.lisp Message-ID: <firstname.lastname@example.org> * Rob Warnock | Actually, to me the "provability" argument is somewhat silly. Sure, I'd | like all my code to be "correct", but IMHO the *real* problem is that | "correct" can only be defined in terms of a specification, and one | thing's for *damn* sure, there's no human way to create "provably | correct" specifications! (Or if you think there is, change | "specifications" to "requirements". Regress as necessary until you get | back to human wants and needs that led to the project [whatever it is] | being instigated. Let's see you "prove" something about *those*!) this argument, which is presented quite frequently, is hard to refute because it makes a number of assumptions that one needs to challenge at their root, not in their application. I'll try, in no particular order. one assumption is that _all_ code should be provably correct, and that in the face of very hard cases one can somehow deduce something about the general provability issues. this is not so. an important argument in verifiable programming is that that which is encapsulated should be verified so you can trust your abstractions. without this requirement, there is no upper bound to the complexity of proving anything, and those who argue against verification (or its costs) frequently assume that they will always deal with unverified code. this is obviously not the case -- people who have worked with these things for years have most probably done something pretty smart to make their work bear fruit, and so the often quite silly arguments about the fruitlessness of their endeavor are only true if you never verify anything. this is somewhat like asking "but how would the stock market work if the government set all prices?" another assumption is that specifications need to be as precise as the program is. this is not so. code contains a lot of redundancy of expression and information and little expression of intent and purpose. specifications should contain what the code does not. in particular, preconditions and postconditions can be expressed (and checked) by other means than computing the value. invariants that are not expressed in code need to be provably maintained. given such intents of the system that never get expressed in code, a specification can be fairly simple, and inconsistencies in a specification are far easier to spot than in a program. yet another assumption is that code would be allowed to be written with the same messy interaction of abstraction levels that programmers tend to use today. this is not going to be allowed. to make verification work, more information must be made explicit, while in most languages amenable to verification, the redundancy in information is minimized. this latter point is also worth underlining: not just any language can be subject to verification. C and C++, for instance, have so complex semantics that it is very hard to figure out what is actually going on unless the code is exceptionally cleanly written. creating correct software is a lot easier than creating buggy software that works. however, if you start with buggy methodologies you'll never obtain correct software, and you might mistakenly believe that correct software is therefore impossible. #:Erik -- religious cult update in light of new scientific discoveries: "when we cannot go to the comet, the comet must come to us."