[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

From: Page, Bill
Subject: RE: [Axiom-developer] Aldor and Axiom (was: SVN on sourceforge)
Date: Wed, 13 Sep 2006 23:56:27 -0400

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.

Bill Page.

reply via email to

[Prev in Thread] Current Thread [Next in Thread]