Re: Software Safety (was: Need help with PowerPC/Ada and realtime tasking)

[bobduff@world.std.com (Robert A Duff)]

In article <dewar.833504787@schonberg>, Robert Dewar <dewar@cs.nyu.edu> wrote:
>What's the point of degrading this useful technical term this way. By
>your definition, correct just means good or some such subjective term.
>The concept of obeying a formal specification is a useful one, and it
>is one which has been given the name "correctness" in the programming
>language area.

Well, I would prefer to call this useful concept "obeying a formal
specification".  At least people ought to say "correct with respect to
formal spec X", rather than the shorthand "correct".  I must admit that
my opinion is pointless, since, as you say, the term "correct" is well
established, and nobody's going to listen to just *me*.

The reason I object to "correct" is that I've seen many cases where
people misunderstand the term.  Even people who ought to know better.
I've seen arguments along these lines: "I proved so-and-so program
correct.  Therefore, it obviously can't have any bugs, or do anything
wrong.  Therefore, there's no need to test it."  A bogus argument, but
it's easy to fool people with that sort of argument, because "correct"
really does mean "good" or "perfect" in plain English.

>I admit is occasionally confusing when standard English words are (mis)used
>in a specific technical way, but as long as everyone understands the
>usage (and correctness has been used in this specific way for many years),m
>then it is useful (after all the Ada 95 RM is full of normal English words
>used in a non-standard way :-)

Sure, but it's not so bad when a more-or-less neutral term is "misused"
that way -- the term is just gaining a new meaning, and one can
(hopefully) tell which meaning is meant from context.  It's much more of
a problem when the English term being hijacked has moral connotations,
as does "correct".

By the way, I suspect that proof techniques would be *more* popular
today, if the proponents had not been overselling their case for all
these years (e.g., saying that proofs avoid the need for testing, and
using loaded terms like "correct" to describe what they're doing).

- Bob