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

[C Y]

--- "Page, Bill" <address@hidden> wrote:

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

I suppose so.  I was wondering if perhaps academic interest in such a
project might be generated - there are a number of teams around the
world working on related tasks.
 
> 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.

Yes, Ocaml would make the possible heavy use of COQ a very interesting
possibility.  My biggest reservation is that the Ocaml compiler is
licensed under the Q public license with some exceptions, but I guess
that's a lot better than not having it available at all.

Haskell seems to have ghc, which looks to be licensed pretty much like
Axiom itself, but the juicy COQ incentive isn't there.  There's
something called Yarrow but it doesn't seem to be as "big time" as coq.

Anybody have experience with these languages?

Cheers,
CY

__________________________________________________
Do You Yahoo!?
Tired of spam?  Yahoo! Mail has the best spam protection around 
http://mail.yahoo.com