Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!swrinde!elroy.jpl.nasa.gov!ncar!noao!arizona!gudeman
From: gudeman@cs.arizona.edu (David Gudeman)
Newsgroups: comp.lang.misc
Subject: Re: Formal definitions (Re: ada-c++ productivity)
Message-ID: <1726@optima.cs.arizona.edu>
Date: 11 Apr 91 03:49:53 GMT
Sender: news@cs.arizona.edu
Lines: 53

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.

]  We used to hear this argument from radio hobbyists who would grab the old 
]  breadboard, a handful of tubes, and a soldering iron and DISCOVER a 
]  circuit.  I trust it as much as I trust a bridge which was built by 
]  sticking together available beams however the designer thought they fit 
]  well.

How is direct experimentation with circuit C less reliable than
(1) experimentation with general circuits followed by (2) theorizing
about the nature of circuits followed by (3) inferences about the
circuit C based on the assumption that the theory is correct?

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.

Also consider that when you have written a program, you can test it to
get some level of confidence that it works.  When you have written a
proof, the only way to "test" it is to let others read it and try to
find problems with it.  (Note that "testing" a proof is not the same
as "testing" a theorem.  You can test a theorem by looking for
multiple proofs, and by looking for contradictions.)

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?
--
					David Gudeman
gudeman@cs.arizona.edu
noao!arizona!gudeman