|
| From: | M. Edward (Ed) Borasky |
| Subject: | Re: [Axiom-developer] Philosophy... |
| Date: | Fri, 23 Sep 2005 23:50:11 -0700 |
| User-agent: | Mozilla Thunderbird 1.0.6 (X11/20050916) |
address@hidden wrote:
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":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.)
http://www.artima.com/weblogs/viewpost.jsp?thread=4639Of 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 ... 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.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.
(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!
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.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.
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
| [Prev in Thread] | Current Thread | [Next in Thread] |