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

[root]

------- Start of forwarded message -------
Date: Fri, 29 Nov 2002 14:47:18 -0500
From: root <address@hidden>
To: address@hidden
CC: address@hidden, address@hidden
In-reply-to: <address@hidden>
Subject: Re: Axiom Journal
Reply-to: address@hidden
X-RAVMilter-Version: 8.3.1(snapshot 20020109) (mail.idsi.net)
X-UIDL: ;(>"!H!6"!;Jd"!#H)"!


> Nelson Beebe wrote:
> 
> Thanks for your detailed response to my comments on the proposed Axiom
> Journal.  

You're welcome. Discussion is good. You're making me think.

> 
> 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?

Actually, I'm not one who subscribes to the "proofs are absolute"
theory. There have been instances of things proven what are later
qualified or disproven. Indeed the standards of proof of the 19th
century are considered as too weak in the 20th. Even mathematics
suffers from this flaw.

As to the size of the proof... There is a certain conceptual distance
between your idea and the implementation. The closer the implementation
is to the machine the larger the gap you need to cross (e.g. writing
in assembler). The closer the language is to the idea the smaller the
gap. Axiom is rather close to the mathematics and far away from the
machine model. That makes the proofs shorter as you are working at
a conceptual level not far removed from the theory and the length
of the proof is the cube of the width of the conceptual gap (daly's thm).
Consider how easy it is to prove something to a fellow prof vs proving
something to a new student.


> 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.

I AM sceptical of proofs of correctness. However, I've tried to prove
programs correct in the past. I find that I learn a great deal more
about my program than I knew before I started. I have no belief that
the program is fully correct but my confidence level was very much
higher after the proof than before.

> 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.  

One of the problems that you run into trying to prove a C program correct
is that you have to have a logical model of the machine on which to
ground the idea of a pointer, for instance. That way lies madness.

We've been looking at MetaPRL and ACL2. The MetaPRL allows you to
"declare theorems", that is make the claim that some function performs
in the manner stated. The plan of attack is likely to start with the
lowest level constructs expressed in Spad (Axiom's algebra code), 
The definitions of BasicType, SemiGroup, Monoid, etc., then to
assume the necessary preconditions, and begin proving from "the
ground up" within the algebra. Thus you have a clearly stated set
of assumptions to start and each algorithm you prove beyond that can
be used as a theorem at the next level.

Since Axiom's libraries are structured in well-defined hierarchies
you can build on all of the previous proofs by using the results
as theorems. In this way you prove Spad algorithms which are fairly
close to the mathematics. 

The big hole in this is, of course, the basic assumptions which are made.
These are made about underlying lisp functions that are called in the
lowest level routines. Failures in these functions invalidate the
chains of proof. However, I would advocate other methods of showing
correctness than trying to recurse into the lisp code.

The small hole in this is, of course, that the proof systems may be
flawed.

In general, it isn't perfect and sometimes isn't even pretty. However,
it does raise the level of confidence in the code. It does give some
assurance that the algorithmic failures are likely to be very subtle
and related to special cases. And it gives a base on which to "debug
the proof" as we get smarter about the process of proving programs.

All of these systems have reached a complexity that is just too hard
for one individual to trust. Mathematica and Maple are "engineering"
systems. That is, they strive to "make it work". Unfortunately this
ends up that subtracting two equal MATRICIES results in an INTEGER 0.

Axiom strives to "make it correct" and follows theory as much as
possible (you at least get the 0 MATRIX). Thus you know what you
SHOULD expect for an answer. The problem is to raise the confidence
that you WILL get the correct answer. Proof is too strong a word in
some sense.

Computer Algebra systems have the advantage that they are modelled on
mathematics. When you try to prove code in other areas, say a text
editor's source code, you have no model of correctness and have to
build one in the logic.  In some sense computer algebra systems are
unique and uniquely qualified as an area of proof.

> 
> 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.

You're certain to know of Dijkstra's comment that you can never prove
anything by testing. Actually, Axiom does run regression testing during
the build. There is a test suite that is used and grows with time.
Every system build runs the test suite and diffs the output reporting
any change.

The pamphlet file format will eventually require two sections, one
of test cases intended for boundary results and one of examples 
intended for user education. However, both of these will be used for
regression testing.

Yet we both know this isn't enough. I'd also like to see the proofs
rerun.

> 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.

There is a second "Axiom" implementation now, called Aldor. The
compiler was written from scratch in C. Axiom is written in Lisp.
They both accept the same input language (modulo platform issues)
so you can test your algorithm in two settings.

> 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.

Yes, I know there has been talk about using the Aldor compiler as a
front-end to systems like Maple. Personally I have little confidence
in the result as Axiom and Aldor have a very strong type system and
other computer algebra systems don't. Statements are ambiguous without
the type system to define the domain. It seems unreasonable to backfit 
the type system into Maple as it goes against the fundamental engineering
philosophy of the Maple system. There are very clever people in this
area, however, and I'm willing to be convinced otherwise.

> 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.  

Well, I see we are of like minds. I've insisted every student of
mine read the mythical man month in every computer course I ever
taught.

> 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

Knuth is likely to be remembered for more things than he can count.
I'm expecting to take a skyload of flak once the source code for
Axiom hits the streets. I'm rewriting it all into pamphlets. The
C, Lisp, Boot, Spad, shell scripts and even the Makefiles have all
been rewritten into pamphlets. There are no other files in the system.
This is certain to cause havoc. I'm gonna blame Knuth :-)

However, I wrote portions of this code many years ago and in some
sense I did it wrong. My code lacks good documentation so it can
be maintained and changed. That may be fine while either I'm the
one maintaining the code or the code is commercial and closed and
maintained by a small team. But once the code "hits the streets"
it would be impossible to train the people to support it in its
raw form. If the code is going to survive for the next 30 years
I've got to "squeeze my brains out onto the desk" and document it.

Documenting the source code directly is wrong because you tend to
write very local, specific comments like "this should work". 
Documenting the code in another file is wrong because you tend to
never revisit that file again. I've "wired" the whole thing
together so that you HAVE to change the documentation in order to
change the source code. The traditional source code is now overwritten
every time the system is changed so you lose your changes if you
change the Lisp code and don't change the document.

I'll just be sure to take a long vacation the day I post the code :-)

Tim

P.S. I'd like to make the discussion public by adding it to the
axiom-mail list if you don't mind. These are points I need to
make anyway with the Axiom community and it would save me a bit
of typing. They probably aren't of interest to the OSCAS list though.
------- End of forwarded message -------