Re: [Axiom-developer] Aldor and Axiom - alternatives?

[Cliff Yapp]

On Wednesday 13 September 2006 11:56 pm, Page, Bill wrote:

> I think that this is so far past our current skill level and
> the available resources that there is virtually no chance that
> this will ever be anything but a paper exercise.

I think it MIGHT be possible for us to make SPAD support the key 
feature or two we want from Aldor (type behavior, etc.) but even 
if we do that, we are still faced with the problem that SPAD as 
a language in Axiom does not have any really good foundation as 
a documented language.   I guess my question to those of us 
looking to improve SPAD is this - even if we can change it to 
support the feature or two we need, how do we document the 
language?  Do we have the resources to make a really formal 
definition?  How do we tie those definitions to something that a 
theorem prover could use?

> If we have to live without Aldor then I think we would be much
> better off looking at possibilities such as how to make Ocaml
> or Haskell work with Axiom. Ocaml at least is heavily used in
> proof systems and has a syntax and object model not too
> different from SPAD and Aldor.

Bill, do you have experience with Ocaml?  Apparently Ocaml and 
Axiom are not completely unaware of each other as projects:

http://caml.inria.fr/pub/ml-archives/caml-list/2005/07/cf19927bddbdfdbb6a062bb9f56262e9.en.html

and apparently there has been some earlier discussion of 
languages + mathematical "fitting":

http://listserv.acm.org/scripts/wa.exe?A2=ind0206c&L=oscas&P=481

Since my guess is some of the people on the list now were 
involved in these earlier discussions, perhaps they can give us 
an idea of what might be the pros and cons of using Ocaml or 
Haskell to re-implement our spad code.

There are some earlier discussions of Ocaml on the list:
http://lists.nongnu.org/archive/html/axiom-developer/2005-10/msg00204.html

Possibly relevant to this discussion:  there has been somewhere 
some work with COQ and Axiom:

 http://www.emis.de/proceedings/MKM2001/hardin.ps

This is probably one of the documents we should look at first, 
but I don't know how to obtain a copy:

1. G. Alexandre. D’Axioma Zermelo. Ph. D. Thesis, University of 
Paris 6, LIP6, February 1998.

To the best of my searching abilities, it's not currently online.  
I suppose a copy might be ordered from the University?

Personally, I am not so afraid of the idea of translating our 
code, since I believe the effort required to understand and 
document properly what is there is going to be almost the same 
amount of effort as a re-write.  Hopefully the interp framework 
is reasonably language independent  (after all we can plug in 
Aldor - which is a separate implementation of a language, even 
if similar to SPAD - already).  Since to make files fully 
literate we need to not only understand the code but the origins 
and definitions of the algorithms being implemented, we are 
looking at a massive effort to spruce up the algebra code no 
matter which way we go on the programming language side.  I 
suspect (although I could be wrong) that understanding and 
documenting properly the design considerations and mathematical 
theory behind the SPAD code will be such a large effort that the 
language considerations become secondary, except for the 
question of what language has the most potential for benefiting 
us at the 30 year horizon.

Cheers,
CY