Re: [Axiom-developer] Philosophy...

[M. Edward (Ed) Borasky]

C Y wrote:

> --- Martin Rubey <address@hidden> wrote:
>  
>
> > > In a sense, Axiom is/was an experiment in the application of
> > > strongly typed programming languages in computer algebra and
> > > to be quite honest and blunt, for the most part the experiment
> > > seems to have failed. :(
> >
> > No, most of it has been transformed into MuPad. However, I dare say
> > that Aldor is superiour to MuPad's language.
> >    
>
> I think the jury is still out on strongly typed issues - such systems
> (including Axiom, in some ways) tend to be designed by experts for
> experts, and thus it is not surprising that in terms of "market share"
> they don't do as well.  I suspect core technical merit has little to do
> with such issues, which is quite unfortunate.
>  
That battle is raging right now in the web development arena, and 
"strongly typed" and "static" languages are taking a beating by dynamic 
environments like Ruby, Python, Perl and PHP. Let's face it ... people 
who program for a living like dynamic languages and hate static ones. If 
the "industry" couldn't hire thousands of inexpensive C programmers, the 
language would have died out except as an "assembler" for dynamic 
language interpreters and the Linux kernel. :)

> If MuPad is using a lot of the ideas that went into Axiom, a) that's
> good and b) we need to do some things significantly different/better
> than MuPad to attract a userbase.  Personally, I think this means
> trying seriously to merge computer algebra with proof systems, and
> creating a computational environment were people can know and prove
> that an answer given by the computer is correct.  Just as security is
> now the great need in operating system and network design, I think
> verifiable correctness and trustable answers and the great frontier for
> CAS.  Feature sets have matured quite a bit over the years, so
> competing on features isn't enough (IMHO).  If we do that, it's hard to
> avoid becoming just another CAS, with a few advantages and a few
> disadvantages compared to other systems.  The net result will be people
> sticking with what they know. (Maple, Mathematica, what have you.)
>  
Well, in the for-profit world, I use Derive. It does everything I need 
at a fraction of the price of the others. MuPad isn't really "free" as 
in either freedom or beer. In the free world, I mostly use Maxima, and 
then only on Linux. Maxima is pretty much useless to me, though, unless 
I also have TeXmacs to typeset my math and mix in text with it.

As to verifiable correctness, a similar situation has occurred in the 
numerical world with such things as interval arithmetic and floating 
point computations based on provable properties of the arithmetic. What 
happens is that the computational cost and complexity of the 
implementation are significant and so it doesn't get done. "Cheap and 
good enough" trumps "expensive and perfect" unless there *isn't* a "good 
enough".

I think you may be seeing the same sort of thing trying to pair CAS with 
proof engines. In a way, your challenge may be worse than the challenge 
of getting verifiable numerical calculations adopted, because both CAS 
and theorem proving rapidly get into NP-Complete and NP-Hard problems, 
whereas the worst-case numerical algorithms in common use are N**4. 
They're both nice dreams for computationalists, though. :)

--

M. Edward (Ed) Borasky

http://www.borasky-research.net/
http://borasky-research.blogspot.com/

http://pdxneurosemantics.com
http://pdx-sales-coach.com
http://algocompsynth.com