I'm Tim Daly, lead developer on Axiom (http://axiom-developer.org)
I came across your opinion page while on the trail of the phrase "The Death of Proofs". That is of interest because I've recently automated Axiom's proof machinery. Axiom is lisp-based and uses ACL2 at that level. The algebra (spad) language is proved using COQ. Now that the machinery is in place, the effort is focused on proofs.
Opinion 26 is about full open source and upward compatible changes. It seems we share the opinion. I fear that computational mathematics based on proprietary software leaves the field open to disaster. Companies die, on average, after 10-15 years. This will be true of computational mathematics companies (witness Symbolics (Macsyma)), (Soft Warehouse (Derive)), (Maplesoft (Maple)), etc. The software internals require huge expertise to maintain and modify but the teams disperse. The software is a major asset so cannot be given away (defunct airlines don't give away planes). The end result, when Wolfram Research does out of business will be a huge black hole in the middle computational mathematics.
I would add that we also need literate programming (LP). Knuth's LP is based on the idea that we should communicate to humans as well as the machine. Computational Mathematics is a "very long term" effort. Several of Axiom's developers are already dead. What they wrote is oft-times inscrutable.
Computation mathematics needs this vital focus. I have, for instance, tried to explain the code for a single algorithm which implements a known formula. Unfortunately the author didn't say which formula (and, as he is no longer alive I can't ask). I have found 20 different formulas on the same subject, none of which seem to correspond to the code.