[Axiom-developer] Philosophy...

[Martin Rubey]

Bill Page writes:
 > On September 22, 2005 5:24 AM Martin Rubey wrote:

 > > > There is an attempt also in Axiom to do the same with input (InputForm
 > > > and SExpressions etc.)
 > > 
 > > I think that this attempt is doomed to fail. Still it may be useful, at
 > > least for debugging.
 > 
 > Could you explain why you think this approach is "doomed to fail"? To me it
 > seems simply under developed in the current version of Axiom. I don't see
 > any conceptual problems with extending the idea. 

Hm. Maybe you are right there. I was thinking at domains like Polytope, where
the representation is not really available to axiom, or at a future Graph
domain. But you are right, in both cases it is probably possible to write a 

coerce: % -> InputForm

 > > > Understanding how to use types and domains [...]  We need to write more
 > > > about this ...
 > > 
 > > No. There is enough written about it (in the Aldor User Guide). A short
 > > introductory text is in the Axiom book.
 > >
 > 
 > ?! I am rather shocked that you would make this claim! :(

 > [...] still I think that types and domains in Axiom are a big problem... and
 > also the main reason to use Axiom as I said above.

What exactly do you think is a problem? I do admit that improving the quality
of the explanations in the Axiom Book would be good, however difficult. Same
for the Aldor User Guide, which is more technical and more detailed. But I
wouldn't write *more* about it. It's too much quantity!

 > It seems to me that one of the reasons that Axiom is not used as much and is
 > not being developed as quick as Mathematica, Maple and even Maxima is
 > precisely because of the problem to trying to understand and use strong
 > typing in computer algebra systems (the marketing and commercial reasons not
 > withstanding).

Look at MuPad, which works well. It has (nearly exactly) the same type
hierarchy as axiom -- still it sells. The difference is mainly the language of
MuPad, which is not statically typed, in contrast to Aldor/Spad.

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

 > > What (good) notation provides is a means to make your ideas and proofs
 > > clear and enable others to follow them. The idea comes before the
 > > notation. Often even the proof comes before the notation.

 > I doubt that "proof comes before notation" because I doubt that rigoursly
 > expressing a proof is even possible without the proper notation. 

I don't disagree, it's probably only a matter of the right wording :-)

I believe (and I think that I know from experience) that sometimes I have the
right idea (intuition), and then I gradually improve notation, sharpen the
idea, improve notation, the idea makes it into a proof, improve notation, the
proof becomes more readable...

I did not claim that "expressing" or "communicating" a proof is (always)
possible without the right notation. (sometimes, it may be, given the right
audience)

Martin