Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!uwm.edu!csd4.csd.uwm.edu!markh
From: markh@csd4.csd.uwm.edu (Mark William Hopkins)
Newsgroups: comp.lang.misc
Subject: Re: Formal definitions (Re: ada-c++ productivity)
Message-ID: <11204@uwm.edu>
Date: 20 Apr 91 04:08:58 GMT
References: <1726@optima.cs.arizona.edu> <29344@dime.cs.umass.edu> <12297@dog.ee.lbl.gov>
Sender: news@uwm.edu
Organization: University of Wisconsin - Milwaukee
Lines: 25

In article <12297@dog.ee.lbl.gov> torek@elf.ee.lbl.gov (Chris Torek) writes:
>To get back onto the topic, then, people advocate `proving programs
>correct' because they believe that the activity really does lead to
>correct programs.  Others advocate testing because they believe that
>testing leads to correct programs.  Both groups are partially right:
>the process of reasoning about programs often turns up bugs, and the
>process of testing often turns up bugs.  Both methods are fallible,
>because they are done by people, and because they make assumptions that
>are sometimes false.

After spending the better part of a week testing software that I have already
proven correct to find bugs that were never in the software but actually a
result of the test conditions not exactly matching running conditions, and
having this happen on *three* consecutive occasions I have no sympathy for
the testing point of view.

If it's proven mathematically, it *will* work.  And if it doesn't, then it's
provably the fault of the underlying hardware (or compiler or assembler).
And yes, I've run into these conditions countless number of times already.

But the point is, after verification, responsibility for proper functioning is
no longer the software writer's job.  That job is complete.

Software is valid, even when it does not function normally due to faulty
hardware or translators.