Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!uwm.edu!linac!att!ucbvax!dog.ee.lbl.gov!elf.ee.lbl.gov!torek
From: torek@elf.ee.lbl.gov (Chris Torek)
Newsgroups: comp.lang.misc
Subject: Re: Formal definitions (Re: ada-c++ productivity)
Message-ID: <12297@dog.ee.lbl.gov>
Date: 19 Apr 91 20:57:40 GMT
References: <1726@optima.cs.arizona.edu> <29344@dime.cs.umass.edu>
Reply-To: torek@elf.ee.lbl.gov (Chris Torek)
Organization: Lawrence Berkeley Laboratory, Berkeley
Lines: 63
X-Local-Date: Fri, 19 Apr 91 13:57:40 PDT

>In article <1726@optima.cs.arizona.edu> gudeman@cs.arizona.edu
>(David Gudeman) writes:
>>Finally, consider the relationship of the proof to the real world ...
>>you will have to deal with the philosophy of mathematical models.

(This goes well off the beam of comp.lang.misc.  You must also deal
with the question of objective reality, and whether, if it exists at
all, it can be perceived.  In order to have useful discussions about
computer theory one has to make a `leap of faith', however justified
that leap may be in one's own experiences, and assume that all this
mathematical stuff really reflects---or perhaps even molds---the `real
world', whatever that is.  For many thousands of words on such subjects
please move to talk.philosophy.* [and say hi to my brother Paul :-) ].)

In article <29344@dime.cs.umass.edu> yodaiken@chelm.cs.umass.edu
(victor yodaiken) writes:
>Not sure what you [DG] 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.

This is actually a better analogy than one might first notice.  We now
believe that Newtonian physics does *not* accurately describe the real
world---but Newtonian physics is nonetheless useful in everyday
situations.  We may use Newton's 3 laws, but we should be aware of
their limits before blindly applying them.

Likewise---and perhaps this is what David Gudeman is talking about---we
can use mathematical models of computer behaviour quite effectively,
but we should keep in mind that they are only models.  Those who work
with hardware will attest to the fact that even a simple NAND gate is
not *really* described by

		 { 0  if a = 0 and b = 0
	a NAND b {
		 { 1  otherwise

(for instance, we have completely ignored the issue of indeterminate
inputs, fan-out, noisy power supplies, and so on).

We make assumptions because that makes the problems we want to solve
tractable.  If we can then `prove' mathematically that the model system
works, we can have some degree of confidence that the real system works
(assuming there is a real system, objective reality, etc.).

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.

My own position on this is that both methods should be used in
moderation, and in proportion to the importance of the problem.  If the
consequences of a bug are minor, it is silly to expend a great deal of
energy avoiding it; if the consequences are serious, it is unwise or
irresponsible not to take safety measures.  Of course, the proper
place at which the line should be drawn is a matter of much dispute.
-- 
In-Real-Life: Chris Torek, Lawrence Berkeley Lab CSE/EE (+1 415 486 5427)
Berkeley, CA		Domain:	torek@ee.lbl.gov