[Axiom-mail] address@hidden: Re: Axiom Journal]

[root]

------- Start of forwarded message -------
Date: Fri, 29 Nov 2002 10:23:37 -0700 (MST)
From: "Nelson H. F. Beebe" <address@hidden>
To: address@hidden
Cc: address@hidden
X-US-Mail: "Center for Scientific Computing, Department of Mathematics, 110
        LCB, University of Utah, 155 S 1400 E RM 233, Salt Lake City, UT
        84112-0090, USA"
X-Telephone: +1 801 581 5254
X-FAX: +1 801 585 1640, +1 801 581 4148
X-URL: http://www.math.utah.edu/~beebe
Subject: Re: Axiom Journal
In-Reply-To: Your message of Fri, 29 Nov 2002 09:54:51 -0500
X-RAVMilter-Version: 8.3.1(snapshot 20020109) (mail.idsi.net)
X-UIDL: `MT!!Rc1"!")6"!fbX"!

Thanks for your detailed response to my comments on the proposed Axiom
Journal.  

I agree that such a journal could offer a distinctively different
publication forum for research in this area.  I'm strongly in favor of
getting software published together with theory.  The computer is
often a harsh and unforgiving judge of correctness, but at least it's
just a machine, and perfectly neutral.

Mathematicians are fond of saying that mathematical proofs are truths
that are absolute, unlike most results in the rest of the sciences.
However, my concern is that logical thinking is very difficult for
humans, and proofs are often so complex that a cynic like me can have
little confidence in their correctness.  Proofs of proofs are usually
bigger than the original proof, so how does one prove the
proof-of-the-proof?

Even simple algorithms and protocols can have exceedingly subtle
points of failure, as Bob Sedgewick's analysis of quicksort showed,
and the recent demonstration of failure of the 1978 Needham-Schroeder
communications protocol.  The latter had stood in the open literature
for about two decades, and was widely taught in computer science
courses, before a problem was discovered in the late 1990s.

If simple tasks like divide-and-conquor, and communications
handshaking, hold such difficulties, then I think that we have to be
very sceptical of correctness claims of more complex statements,
whether they are mathematical, or the ISO network model, or the laws
of most countries.

A correctness proof of a computer program may be nice to have, but it
is not sufficient: one still can have errors in its implementation,
either from the program itself, or from its compilation into some host
machine code, or from errors in its run-time libraries, or in the
network, or in the underlying hardware.  

The engineering solution to problems like this is multiple independent
implementations of portable computer programs that can be run on
multiple operating systems, architectures, and compilers.  Only by
reproducing results with independent studies can we garner confidence
in them.

The growing practice in the free software community of including a
"make check" validation suite in software distributions is a good step
in the right direction: at least then one can have confidence that a
local installation of software is behaving the same way it did for its
original authors.  The idea isn't new: Don Knuth was doing that in the
early 1960s with his Algol compiler: every bug report became a member
of a test suite the ensure that fixes did not get unfixed by later
modifications.

It has long been of concern to me that software written for
single-compiler languages is of necessity suspect: this includes
Visual Basic, C#, perl, python, Macsyma, Mathematica, Maple, Axiom,
Reduce, and essentially all other symbolic algebra languages.  To some
extent, I also include Matlab and S-Plus: octave and R are independent
implementations of those two, but octave at least is not complete
enough to handle every Matlab program.

In the symbolic algebra community, it has so far proven impossible to
automatically translate software from one language into another.
Richard Fateman tried a Mathematica-to-Macsyma translation, only to
discover ambiguities arising from the fact that Mathematica is not
defined by a rigorous grammar.

The lessons of Fred Brooks ``The Mythical Man Month'' and Bruce
Schneier's ``Secrets and Lies'' are that complexity is a huge
impediment to getting things right.  

Don Knuth once told me that he hopes that long after he's gone, the
work that he'll most be remembered for is literate programming,
because he feels that it is the only way to program computers
reliably.  It is sad how little the idea has caught on, as documented
in

        http://www.math.utah.edu/pub/tex/bib/index-table-l.html#litprog

- 
-------------------------------------------------------------------------------
- - Nelson H. F. Beebe                    Tel: +1 801 581 5254                  
-
- - Center for Scientific Computing       FAX: +1 801 581 4148                  
-
- - University of Utah                    Internet e-mail: address@hidden  -
- - Department of Mathematics, 110 LCB        address@hidden  address@hidden -
- - 155 S 1400 E RM 233                       address@hidden                    
-
- - Salt Lake City, UT 84112-0090, USA    URL: http://www.math.utah.edu/~beebe  
-
- 
-------------------------------------------------------------------------------
------- End of forwarded message -------