[EMAIL PROTECTED] wrote:
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.)
Here's a sample of the kind of things developers from the
"agile"/"extreme programming" school of thought have to say on the
subject of "static vs. dynamic":
http://www.artima.com/weblogs/viewpost.jsp?thread=4639
Of course, the "general programming/scripting language" world is very
different from the mathematical rigor world where Axiom and other CAS
and proof engines live. My belief is that the purpose of programming is
to deliver high-quality software as defined by the user. The user of a
web application, like on-line banking, has a much different view of what
high quality is than a user of a CAS or proof engine ... *and* both are
much different than the definition of quality when the user is a
*developer* of on-line banking software or the user is a *developer* of
a numerical package, CAS or proof engine.
But ... well ... Axiom has a Lisp core. And the Lisp
compiler/interpreter has a C core. So does the Gnu Compiler Collection. :)
I think it's important to automate as much as is possible of *every*
knowledge worker's job. This is the computer as "intelligence
amplifier". The job of a mathematician (leaving aside the important
distinction between theoretical and applied!) is to get correct results.
So as a sometimes applied mathematician, I think the combination of CAS
and proof engine is a good idea, and the discipline of strong static
typing and a complier that can catch lots of bugs in one project while
I'm working on another project makes my job easier, not harder.
On the other hand, as a practicing performance engineer and capacity
planner, there are times when I have to grind through gigabytes of
performance data and do a queueing model. Then I want a programming
environment that allows me to bang out a quick solution that executes
efficiently and gives me visualizations that tells me what's going on.
For that, I use Perl and R and, increasingly, relational databases. I
could probably replace R with Axiom, but I'm guessing I'd still need the
Perl component.
I've done a little "number crunching" in Derive. It works surprisingly
well, actually -- if my colleagues were mathematicians or physicists
rather than managers and software engineers, I'd do all but the largest
problems in a CAS, provided it had a good typesetting engine like
TeXmacs. Derive isn't all that bad at typesetting, but it's nowhere near
as "pretty" as TeXmacs with an Axiom or Maxima session.
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.
Well ... I don't know ... have you looked at the Maxima road map
recently? They've been at 5.9.1 for what seems like ages, and what they
want in 6.0 is huge! Axiom, Maxima and Reduce are the old war horse CAS.
Derive was born on a TRS-80, grew into a strong adolescent on DOS and
now runs on Windows. I don't know too much about Maple or Mathematica; I
"almost" learned Maple but it was way too slow on a 25 MHz Motorola
88100 with 32 MB of RAM for any practical use.
(Yes, Derive really was born on a TRS-80, a 64 kilobyte Z80 machine with
a cassette I/O subsystem.) :)
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.
Might I suggest heading over to this web site:
http://headrush.typepad.com/creating_passionate_users/
The MathAction / Axiom front page is exactly what you need to create
passionate users!
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.
Well ... if it's any consolation, the core of what Google does very well
is a singular value decomposition. Somebody besides the
military-industrial complex finally got rich with computational linear
algebra. :) Spreadsheets ... been done. Word processing ... been done.
Web 2.0 ... being done. Searching, the semantic web ... been done.
How about biotechnology, though?
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 :-/.
Oh, it's worth doing ... my dreams when I got out of grad school (1974)
were to own a computer capable of algorithmic composition and synthesis
of music, and to have a computer prove the programs I wrote for a living
were correct. One out of two ain't bad! :) It's worth doing ... so is
solving the halting problem. :)
--
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
_______________________________________________
Axiom-developer mailing list
[email protected]
http://lists.nongnu.org/mailman/listinfo/axiom-developer
