Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!sun-barr!lll-winken!elroy.jpl.nasa.gov!swrinde!zaphod.mps.ohio-state.edu!rpi!bu.edu!m2c!umvlsi!dime!yodaiken
From: yodaiken@chelm.cs.umass.edu (victor yodaiken)
Newsgroups: comp.lang.misc
Subject: Re: Formal definitions (Re: ada-c++ productivity)
Message-ID: <29344@dime.cs.umass.edu>
Date: 16 Apr 91 12:37:04 GMT
References: <1726@optima.cs.arizona.edu>
Sender: news@dime.cs.umass.edu
Reply-To: yodaiken@chelm.cs.umass.edu (victor yodaiken)
Organization: University of Massachusetts, Amherst
Lines: 51

In article <1726@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:
>In article  <969@mgt3.sci.UUCP> D. C. Sessions writes:
>]  Of course, I can't *prove* that a transient error was due to substrate 
>]  injection resulting from pin overdrive.  Since I can't prove it, let's 
>]  forget the whole thing, right?
>
>That isn't a parallel situation.  If you can show that some insecurity
>exists in a program then it should be fixed.  That does not mean that
>it is useful to try to prove mathematically that there are no
>insecurities.
>

Why not?  

>
>I think that this "faith in formalism" betrays a lack of thought about
>the philosophy of science, math, and models.  Not that I blame you for
>this.  The fault lies with modern university educations which -- at
>least in the US -- are painfully lacking some important foundational
>studies.
>
>Can anyone who thinks it is useful to "prove" programs correct provide
>me with an explanation of exactly what the proof accomplishes?  What
>do you know after the proof that you didn't know before the proof?
>Before you answer, consider this: the process of deriving a
>mathematical proof is every bit as prone to errors as is the process
>of writing a computer program.

I want to write, say, a real-time process synchronization program
that will allow distributed process control programs to communicatate.
Before I begin to code, it seems only reasonable that I should be
able to describe the proposed algorithm, the assumed time costs
of key operations, and the correctness requirements, and then prove
that the algorithm can work. A chunk of Scheme, "C", or any other code
will not be very informative here. 


>Finally, consider the relationship of the proof to the real world,
>what assumptions are essential to this relationship, and whether those
>assumptions are more reliable than the reliability that you can get by
>direct testing.  To answer this question you will have to deal with
>the philosophy of mathematical models.  What relationship does the
>concept of a "set" have in common with the real world?  Sets follow
>strict rules, how can we know that anything in the real world follows
>any rules similar to those for sets?


Not sure what you are getting at here. Of course mathematical notions are
just abstractions from reality. But, they may be useful abstractions. 
An apple does not care about Newton's laws, but the laws give us a good
tool for understanding how the apple might fall.