Re: [Axiom-developer] Comparison of CAS's?

[C Y]

--- Vladimir Bondarenko <address@hidden> wrote:

> I am shocked to observe that it looks like AXIOM developers have
> an idea that "there are not so many defects in AXIOM".

I don't think this is the case - rather, we feel that Axiom has the
long term potential to provide a robust environment on which to build. 
The system in its current form obviously has many defects.
 
> If you will keep thinking the same way forgetting about the quality
> assurance problems, you never reach your 30-years goal of getting a 
> powerful dependable AXIOM.

That goal requires foundational work before it can be practically
attacked.  In particular, either SPAD or Aldor (whatever is ultimately
chosen) MUST be clearly and precisely defined.  Arguably, we also need
to integrate either ACL2 or some other such system as well - eventually
we should provide the ground work for provable correctness.

Quality assurance is necessary, but it is not sufficient to have total
confidence in a system.  What IS required to have total confidence in a
system is still (as far as I can tell) a legitimate subject for
research.  Some people feel this is not a possible goal, but my hunch
is that computer produced results can achieve a level of trustability
that would compare favorably to human correctness auditing. MAKING that
system is an immense challenge, but the potential benefits are also
immense.

> Frankly, a big problem I see, there is not a single practical
> QA engineer within AXIOM folks.

To be honest, I don't think we are at that stage yet.  Attacking the
Algebra in a major way will come once we have a foundation within which
we can attack it successfully (i.e. with some confidence solutions to
problems will remain viable in the long term.)  The resolution of the
SPAD vs. Aldor decision is an obviously critical step in that process.

QA starts when there is expectation that the product you have can meet
such tests successfully - if you KNOW it can't, then there is little
point.  You fix what you already know is broken, and then when you
think you have it you hit it with QA testing.  We have a Long List of
things that we know are broken.

Paul Dietz wrote a very interesting utility which generated random
valid lisp code as a way to stress Lisp compilers and their compilance
with the ANSI standard.  Perhaps a study of that code would suggest
ways to do something similar for mathematical problems.  But I
personally have no expectation that Axiom is ready for that level of
testing - that comes later in this process.

Cheers,
CY


       
____________________________________________________________________________________
Yahoo! oneSearch: Finally, mobile search 
that gives answers, not web links. 
http://mobile.yahoo.com/mobileweb/onesearch?refer=1ONXIC