Re: [Axiom-developer] Philosophy...

[smustudent1]

On Thursday 22 September 2005 11:40 pm, M. Edward (Ed) Borasky wrote:
>
> 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. :)

Well, to be fair, I think it's a question of what the programmer is trying to 
accomplish.  For quick prototyping and getting ones ideas into workable for 
as rapidly as possible, I agree dynamic languages are probably the tool of 
choice (e.g., Lisp.)  For doing something as correctly as possible, however, 
I'm not so sure.  I think the CAS field is a bit unique currently in being 
really interested in correctness.  (Or at least, some parts of it.)

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

Right - Axiom doesn't have enough mindshare right now to challenge even Maxima 
in "popularity."  I would argue that this isn't necessarily a bad thing - I 
would expect Axiom to be less of a "phenomenon" until it reaches a point 
where it is competitive, which will take longer when developing for 
correctness is the first concern.

> 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'm hoping open source will allow us to short circuit those economic 
limitations to some extent.  If we can create a really good system, perhaps 
we can move the "good enough" yardstick further out.

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

Well, dreams are what great accomplishments start as :-).  I think both 
verifiable numerical computations and smart integration with proof systems 
could go a long way towards making Axiom not just another entry in the CAS 
market but a fundamentally new type of software - maybe even a "killer app" 
in relevant mathematical and scientific areas.  

Of course, I'm not really qualified to have dreams like this yet :-).  Maybe 
after a few years of studying up on the issue I'll know why it's not worth 
doing :-/.

Cheers,
CY