Re: [Axiom-developer] Can you depend on it?

[C Y]

--- address@hidden wrote:

> Ah, that's the question for today...."Can people depend on it?".
> 
> And if they can't know the results are correct, what's the point?

That combination of questions might be the most common objection I have
heard to using CAS software in science and mathematical research.  One
I happen to agree with. Oh, there are others, such as the tendency of
lazy humans to substitute computer software for understanding, and that
has its valid points, but the most serious one I think is being able to
know the results are correct. 

> I believe that Axiom could be the foundation for the next few hundred
> years of computational mathematics. Oh, not the program we have
> now. But the one it could evolve into if we do it right. Axiom is the
> only program I've ever worked on that has that potential. The
> mathematics doesn't change and, if correctly implemented, Axiom
> should always give you an answer you can depend on. In fact, you
> should be able to look at the final result of an Axiom computation
> and KNOW it is right. And after that time, you and everyone else can
> depend on it. Like an aircraft wing, only better because this is
> mathematics.

This is why I think it is important to pursue proof checkers (things
like Isabelle, HOL, COQ, ACL2, etc.) as a starting point, not as
something to tack on later.  KNOWING a result is correct when a
computer produces it is very very complex.  It is unambiguous when a
wing breaks, and fairly easy to measure (given the right equipment). 
Predicting it is fairly hard, but doable.  Ditto for the robot - if
something goes wrong, lots of equipment starts flying that shouldn't be
moving.  Or, in the less spectacular case, the wrong thing gets welded.
 A computer has many subtle points of possible failure.  Is it a weird
CPU bug, a mishandling of information in some subtle, unexpected way, a
1/1,000,000,000 failure condition of the operating system (think the
blackout that hit most of the northeastern US a while back - they
traced that back to a software error condition with a very small
window: http://www.securityfocus.com/news/8412)  If the systems running
such a major portion of the national energy grid can't be completely
trusted, why should anyone trust CAS software?
 
> But I also find it frustrating because I don't see any Bill Perzley's
> in the game. Bill not only learned the mathematics (we both took the
> same course from Lou Paul), he understood it. He "programmed" it (we
> didn't have anything but calculators and switches for programming but
> it was still programming). He wrote it up so *I* could understand it.
> And when he wrote programs they worked and *I* could check them. You
> could bet your life on his work. And Bill often did.

In this instance, it sounds like both the hardware and software were
special purpose, very well engineered, and he had a fair amount of
time/money to commit to the project.  While authors of CAS systems
might be able to make sure the software they write is solid (although
that goal still seems a ways off) they must rely on both the operating
environment and the hardware underneath it to work correctly.  Neither
of those components is under the control of the author, since the
software will be installed in as many environments as it can be made to
run.  It will work most of the time, but who knows when some subtle
difference will trigger a northeast blackout in the results?  How can
it be prevented?

> Is this the level of quality we see in Axiom? Nope. Is this the level
> of quality we can achieve? Yes. So, why don't we achieve it? Why
> don't we write Axiom software as if our life depended on it? Why are
> we still writing software like the Chandler project? Why can't we say
> that this WILL work and it WILL give you the correct answer?

Because, among other reasons, we don't have the tools that will let us
make that assertion and back it up.  I doubt Perzley would have been
willing to do what he did if the robot was being operated by Windows XP
and was just taking instructions he had fed it - I know I sure wouldn't
- because every element of the system which MIGHT cause failure isn't
guaranteed.

> What does it take to get Perzley kind of quality?

This is the type of problem I would like to do research in, someday.  I
have a ways to go first (as you mentioned earlier, you must know both
the mathematics and how to program, and I am working on increasing my
basic knowledge before making another run at Axiom level problems) but
the question is a worthy one.

Science magazine had a rather interesting article (I suppose it's not
the full story since it's a specialty topic in a general magazine, but
I found it good food for thought) about the difficulties that have
begun to appear in the form of proofs that cannot be checked by human
reviewers: 
http://www.sciencemag.org/cgi/content/summary/307/5714/1402a   In that
article, the point was made that there are two aspects to proof
checking:

1.  Knowing it is correct
2.  Understanding why it is correct (human understanding)

If you only use human beings to check proofs, these two components are
not separable.  A human being must understand the proof in order to
know if it is correct.  An automated proof checker, correctly done,
should be able to mechanically verify that the proof is sound.  In
theory, a human being dogged enough to follow the computer through the
steps should arrive at the exact same conclusion, although the
experience is unlikely to build much insight into how to make "good"
proofs.  What needs to be human understandable is a) the proof checking
system and b) the logic converting human CAS style inputs into proof
statements.  Once the correct proof statements are generated, the proof
checker will take it from there.

I think the distinction is important for what we are trying to do here,
because for a CAS it is less important to produce elegant/beautiful
proofs and more important to know the result is correct.  Proof
software may never generate the "optimal" proof for a given result, but
so long as it generates a CORRECT proof that can be evaluated in
reasonable time it has done what is needed for us to rely on it.  In
our case the proofs are a means to an end - if people can rely on
Axiom's results as having come from components that have proof backing,
and can at need (say for a particularly critical result for a paper)
have Axiom generate the full proof validation for a result to be
verified by any of several systems, I think we will have achieved a
level of confidence that will permit more general use of the systems. 
We will be able to say "yes it is correct, and here's the proof, to be
checked however you care to check it."

Now the details of that system, and whether it is even possible, are
the subject of many years of fascinating research and may even require
defining as unambiguously as possible what it means to prove something.
 But I think this is going to be essential for the long term viability
of any such system - it must be "so good" that using anything else
becomes a liability.

CAS systems are currently used in science - Mathematica + Feyncalc was
a common tool at my undergrad physics department - and those systems
have become usable through a sort of prolonged process of evaluation by
many scientists.  However, if asked to show proof that a feyncalc
derived result was correct, pencil and paper work would be needed to
verify the system was correct.  Making a system that WOULDN'T need such
work is going to be a hard sell, and some good answers to the question
of why any new system is any better than Mathematica + Feyncalc would
be needed.

But to make that system, one must know not just programming and
mathematics but proof logic as well (plus high energy physics, for this
problem domain), and how to make all of them interact.    Which reminds
me, I have some reading to do...

Cheers,
CY


 
____________________________________________________________________________________
Don't pick lemons.
See all the new 2007 cars at Yahoo! Autos.
http://autos.yahoo.com/new_cars.html