RE: [Axiom-developer] Aldor and Axiom (was: SVN on sourceforge)

[Page, Bill]

On Wednesday, September 13, 2006 11:46 PM Cliff Yapp wrote:

> ...
> [no Aldor open source license] 
> This of course does not mean that we cannot learn from and
> use the ideas in Aldor - merely that we must take our SPAD 
> beginnings and build them up into something better.
> 
> If we must do this, I would like to see some thought put into 
> designing and defining SPAD+ or whatever with an eye towards 
> formal proving systems and automatic proof generation.
> ...

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.

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.

Regards,
Bill Page.