[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiom-developer] RE: FW: summer of code
Re: [Axiom-developer] RE: FW: summer of code
Sat, 14 Apr 2007 00:23:06 -0400
Thunderbird 188.8.131.52 (X11/20070308)
Bill Page wrote:
> It feels rather odd to me to be able to point out that Lisp
> is well past that original 25 year horizon and it is still
> essentially the same language as it was - dialects and various
> libraries not withstanding.
Indeed - IIRC it is up there with Fortran in terms of age.
> But then what we are really talking about here is mathematics
> and many of the algorithms that we are implementing in our
> computer algebra systems are actually based on mathematics that
> was developed as much as a *hundred* years earlier. Perhaps
> Lisp is a little like that - more mathematics than a trendy
> programming language.
Exactly - that is what appeals to me about making Axiom's math level
programming as much like "actual math" (whatever that means, we're still
exploring that I think) as possible. If we really do the job well, the
result should be timeless. I view TeX as a good example of this - it
solves its targeted problem so well that it has lasted for decades and
is still going strong. Even if a new system should replace it the
design decisions and algorithms are likely to live on. Axiom has the
potential to do the same thing for mathematics, and that is what makes
it such an exciting project for me. I hate doing things more than once
- it's a waste of effort and it shouldn't be necessary except for
teaching/learning. Axiom has the potential to let people solve problems
once, correctly, and then build off of them in a way that is convenient,
rigorous and scalable.
> So I wonder about Axiom. Are the design principles on which it
> is based firm enough to be relevant over the long haul? Perhaps.
If not, we will upgrade to better ones as we discover them. Even if we
aren't optimal now, I think Axiom is close enough that we can profitably
build on it as a starting point.
> And here Axiom is now, nearly 30 years after it's inception. But
> then Maxima (formerly Macsyma) is a system of the same time period
> as Axiom and it is still alive today. We need something else to
> explain that.
That is not particularly difficult. 1) The original researchers are
still available to work on it, which helps fuel the community 2) it was
open source before Axiom, and so built a community while it was the
"only game in town" 3) it is more of an "engineering" system at the
moment in that it focuses less on mathematical typing et. al. and more
on "getting the answer that is useful." (Axiom may someday do that as a
special case of being correct, but it's not there yet.) 4) It
integrates better with other tools (gnuplot and wxmaxima) that people
find convenient to use for practical work they need to get done now.
Maxima is what you look to if you want a free Maple/Mathematica. Axiom
is a new breed and currently requires more of an initial learning
investment. Eventually Axiom may adsorb or surpass Maxima's abilities
and be attractive to a broader audience but IMHO that will come later
(and should come later, as we have Maxima to handle those needs until we
are ready to offer something demonstrably better for the applications
needing "engineering" CAS.)
> I agree it is incredible but I have serious doubts about the
> rest of your claim. I don't know what "good enough" means. I am
> afraid that your model of development means just a lot of people
> re-inventing the same thing in essentially the same way according
> to the current fashion. I think that is a form of entertainment
> but not real progress.
That is true to an extent (just look at the number of graphical toolkits
and window managers for X...) but I think it is less true for more
complex software. Blender, for example, does not have serious
competition in the open source world that I am aware of. Nor does
BRL-CAD. (Of course, those both started as closed source packages but
that's another post...) Even if someone wants to re-code it in a
different language the research into the algorithms in projects like
this is re-used out of necessity.
I do not expect that people will begin working on heavy duty CASs in the
sense of trying to duplicate Axiom from scratch. The problem is too
difficult - it is one of the few cases where learning the existing tool
is unambiguously easier than re-creating it (a problem with more basic
tools/libraries, especially in Lisp it seems...)
> On the other hand, Axiom as a project with a 30 year time
> horizon is very different. The system design on which we are
> working today is essentially the same as the one originally
> envisaged nearly 30 years ago.
Which is encouraging, because it means we may have a well defined
project idea here :-). I'd say that longevity is a sign of strength.
> Besides saving 30 year of
> intellectual effort from the trash bin, we are mostly trying to
> carry on the same programme: to encode more mathematics in the
> form that can be manipulated by a computer and at the same time
> trying to "sell" the basic idea to people who have not yet
> realized that the problem it is trying to solve even exists!
That is a very interesting point and I wonder if it will be one of the
major formative changes in the field over the next 100 years of
mathematical research - the pursuit of assurance of correctness without
direct human mechanical verification. The human mind has limitations
and there may be interesting and useful correctness proofs that are
intrinsically beyond the ability of any one human mind to verify. But
if we can verify a verifier and trust that verifier, we can know the
proof is real. (After all, if we accept a review of a proof as correct
we are trusting the minds of the reviewers to be accurate.) CASs offer
convenient ways to solve problems today, but they are not yet better
than human minds at being correct/verified. I hope someday Axiom will
be - just as we can only see into the depths of the universe with tools
beyond our own senses, we may find ourselves gazing into the depths of
mathematics with mechanical tools more capable of recognizing
correctness of large scale proofs than our own minds.