Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!mips!spool.mu.edu!snorkelwacker.mit.edu!bloom-beacon!eru!hagbard!sunic!sics.se!fuug!news.funet.fi!jyu.fi!sakkinen
From: sakkinen@jyu.fi (Markku Sakkinen)
Newsgroups: comp.lang.misc
Subject: Re: Formal definitions (Re: ada-c++ productivity)
Message-ID: <1991Apr12.075520.25394@jyu.fi>
Date: 12 Apr 91 07:55:20 GMT
References: <1726@optima.cs.arizona.edu>
Reply-To: sakkinen@jytko.jyu.fi (Markku Sakkinen)
Organization: University of Jyvaskyla, Finland
Lines: 66

In article <1726@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:
>In article  <969@mgt3.sci.UUCP> D. C. Sessions writes:
> ...
>]  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?

And how is something like Newton's law of gravitation more reliable
and useful than experimenting with each pertinent object separately?
"That ball fell onto the ground when I left hold of it ...
by golly, this glass bowl does the same!"

>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?
> ...
>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.  [...]

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?

If the Fortran source read like this:
      FUNCTION ADD (I, J)
      ADD = I + J
      RETURN
      END
I would have very high confidence that the function is all right.
On the other hand, if there were additionally a statement like
      IF (DAY(TODAY) .EQ. 13) ADD = ADD - 3
I would promptly "prove" that the code will not do what was promised.
Even exhaustive testing would not discover that unless one should
happen to test on the 13th of some month.

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.

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.

Markku Sakkinen
Department of Computer Science and Information Systems
University of Jyvaskyla (a's with umlauts)
PL 35
SF-40351 Jyvaskyla (umlauts again)
Finland
          SAKKINEN@FINJYU.bitnet (alternative network address)