Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!usc!sdd.hp.com!news.cs.indiana.edu!arizona.edu!arizona!gudeman
From: gudeman@cs.arizona.edu (David Gudeman)
Newsgroups: comp.lang.misc
Subject: Re: Formal definitions
Message-ID: <1823@optima.cs.arizona.edu>
Date: 12 Apr 91 18:29:27 GMT
Sender: news@cs.arizona.edu
Lines: 90

In article  <1991Apr12.075520.25394@jyu.fi> Markku Sakkinen writes:
]In article <1726@optima.cs.arizona.edu> David Gudeman writes:
]>How is direct experimentation with circuit C less reliable than...
                                                    --------

]And how is something like Newton's law of gravitation more reliable
]and useful than experimenting with each pertinent object separately?
     ------

Newton's law is _less_ reliable than direct experimentation.  Draging
"useful" into it strikes me as a transparent attempt to change my
meaning.  Of course formalism is useful in some circumstances -- did I
mention that I consider myself primarily a theorist?  My view on
formal proofs of correctness is not from a super-pragmatic disdain of
formalism, it comes from contemplating the nature of formalism.

]Suppose someone says he has written a procedure that takes two
]integers and returns their sum as result.  Would you really prefer
]to test it (exhaustively:  in a 32-bit computer, 2**64 additions
]take a lot of time;  quickly:  add (1, 1) returns 2, add (1, 2)
]returns 3, I guess this really is an addition procedure)
]to a "proof":  reasoning about the source code?

I reject both of your methods of test, neither is what I call testing.
Furthermore, it is obviously necessary to reason about the source code
but that is not the same thing as a formal proof of correctness.  A
formal proof of correctness involves a sequence of written expressions
in another language --distinct from the programming language-- that
purports to "prove" that the program meets some specification, also
written in a formal language.  The question is how writting proofs in
this other formal language is better than testing the program
directly.  I claim that it is not.

(I also claim that in general writing specifications in a formal
language is superflous.  Please note that "in general" is not the same
as "universally".  Specific examples where a formal specification is
useful are not going to influence my opinion.)

]      IF (DAY(TODAY) .EQ. 13) ADD = ADD - 3
]I would promptly "prove" that the code will not do what was promised.

It doesn't take a formal proof in a different language to see the
problem, as shown by the fact that you assume I will see the problem
without such a formal proof.

]Even exhaustive testing would not discover that unless one should
]happen to test on the 13th of some month.

To do testing correctly, you have to take into account the nature of
the code being tested.  If the code has a conditional as above then
you had better test it both on a 13th and on other days or you have
not tested correctly.

]Many authors through the decades (I don't know who was the first)
]have pointed out in the literature that testing computers and software
]is tremendously more difficult and less conclusive than doing physical
]experiments and measurements, because software and digital hardware
]can have utterly discontinuous behaviour.

Nonsense.  Testing software is much easier than physical experiments.
You have complete control over the environment and you can guarantee
that the test subject (the program) is identical to the previous
subject.  In physical experiments things wear out, dirt gets into
parts, loose coat sleeves throw things out of alignment...  This
discontinuity in behavior in computers is an _advantage_.  It lets you
ignore history.

]I may interpret you incorrectly, but here
]you seem to have an attitude similar to James H. Fetzer,
]who in his article "Program verification: the very idea" (CACM,
]September 1988) stubbornly refused to view source code as an entity
]distinct from its execution on a concrete computer.

I'll have to look up the article, maybe I'm not the only one who sees
that the emporer has no clothes.

I'm willing to view source code as a distinct entity, I accept the
usefulness of languages semantics and even formal proofs of
correctness in some circumstances.  My argument is that these formal
proofs do not give the same level of confidence that testing does.
And further, that anyone who thinks that formalism gives more
confidence than testing has not thought enough about the nature of
formalism.

I have yet to see a defense of formal proofs of correctness that deals
with my philosophical objections.
--
					David Gudeman
gudeman@cs.arizona.edu
noao!arizona!gudeman