From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.3 required=5.0 tests=BAYES_00,INVALID_MSGID autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,59dddae4a1f01e1a X-Google-Attributes: gid103376,public From: dewar@cs.nyu.edu (Robert Dewar) Subject: Re: Software Safety (was: Need help with PowerPC/Ada and realtime tasking) Date: 1996/05/30 Message-ID: #1/1 X-Deja-AN: 157698344 references: <63085717wnr@diphi.demon.co.uk> <31AC0712.29DF@lmtas.lmco.com> <31AD794D.2E62@lmtas.lmco.com> organization: Courant Institute of Mathematical Sciences newsgroups: comp.lang.ada Date: 1996-05-30T00:00:00+00:00 List-Id: Bob Duff said (if I have not lost track of who said what :-) "> I suppose it depends on your definition of "correct". The > proof-of-correctness folks define "correct" to mean "correctly obeys the > formal specification". To me, that's a bogus definition. In plain > English, a "correct" program is one that does what it's supposed to do, > regardless of whether the specification is wrong. If you show me a word > processor that deletes my file when I told it to italicize a word, to > me, that's incorrect, even if you can show me a (bogus) formal spec that > says that the "italicize word" function should delete files. If you > show me a flight-control program that crashes airplanes, that's > incorrect IMHO, despite the fact that you might show me a formal spec > saying it did what the formal spec says." 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. 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 :-)