Re: Should I learn C or Pascal?

[srt@zaphod.csci.unt.edu (Steve Tate)]

Robert Dewar (dewar@cs.nyu.edu) wrote:
> Steve said

> "| poster.  To explain that a little better: you can never, EVER "test
> | the correctness" of an *algorithm* by executing it.  I don't care how
> | you design your test cases, the ONLY way to show the correctness of an
> | algorithm is with a formal mathematical proof.  Of course,
> | implementations are good for demonstrating the INcorrectness of some
> | algorithms!  :-)"

> Well it is a reasonable guess that Steve is pretty new to the field and
> is repeating what he has been taught. 

Ummm... no.  I've been programming for about 18 years, and have had a
Ph.D. and been teaching for about 5.

> But still, this concentration on
> correctness seems a mistake to me, and it particularly seems a mistake
> to concentrate on correctness to the exclusion of pragmatic understanding
> of the real issues.

> Steve, you need to understand that correctness is just one aspect of a 
> program. Correct programs are not necessarily usable or acceptable, and
> incorrect programs are often both usable and acceptable. There are two
> issues here.

And you seem to have totally missed what I said.  Nowhere (not even
once) did I say anything about proving that a *program* was correct.
I was talking about correctness proofs for *algorithms*.  Take, for
example, Prim's algorithm for finding a minimum spanning tree.  There
are a huge number of different ways you can implement this, using
different data structures or different languages, but the abstract
sequence of steps that makes it Prim's algorithm is very well
defined.  Furthermore, you can formally prove the correctness of the
algorithm which, of course, doesn't depend in the least on
implementation details such as exact data structures of programming
language.  I think using a real programming language to describe
Prim's algorithm would be a mistake because it wouldn't clearly
emphasize that these details are not relevant to what "Prim's
algorithm" really is.

Let me give you another example that better illustrates what I said
about an implementation telling you nothing about the correctness of
an algorithm.  There is a proposed primality testing algorithm (based
on a sequence of numbers called the "Perrin Sequence") which was
recently (June 1996) described in Scientific American.  The algorithm
has been known for about 100 years, but noone has been able to either
prove that it works correctly or give a counter example.  There have
been implementations, and for almost a century all empirical tests
have shown that the algorithm works.  Until a couple of weeks ago.
That's when a counter example was found.  So I repeat what I said
before: you can tell absolutely nothing about the correctness of an
algorithm by testing --- the only thing that reasonably shows the
correctness of an algorithm is a good mathematical proof.

> Correctness only reflects the match between a program and it spec (Note; i
> know we had a discussion about the confusion caused by taking a general
> term like correctness and using in this restricted sense, but that is clearly
> what Steve is talking about when he talks about a mathematic proof, since
> clearly you cannot proove a program correct if you use the more general
> informal meaning of correct :-)

Again, I was talking about algorithms, not writing a program "to
spec".  When you talk about algorithm, you are normally given a clear,
unambiguous, mathematical description of what needs to be computed.
Proving correctness is clearly desirable in such a situation.

--
Steve Tate  ---  srt@cs.unt.edu | "As often as a study is cultivated by narrow
Dept. of Computer Sciences      |  minds, they will draw from it narrow
University of North Texas       |  conclusions."  -- John Stuart Mill, 1865.
Denton, TX  76201               |