RE: [Axiom-developer] Aldor and Lisp

[C Y]

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

> On Tuesday, October 18, 2005 10:15 PM Camm Maguire wrote:
> > 
> > Bill Page writes:
> > > 
> > > In fact to take best advantage of this knowledge, perhaps we
> > > might seriously consider the possibility of writing "new Aldor"
> > > in a language like Ocaml.
> > > 
> > 
> > Can't believe this thread has come full circle like this! Wow.
> 
> Perhaps I should have written my previous comment with a ;) because
> in a sense I was only "half serious". The main point I wanted to
> emphasise was that writing a new compiler was a big and difficult
> job. The skills required to do it properly and according to modern
> practices require some familiarity with other modern advanced
> programming languages. One way to ensure this would be to write it
> in such a modern advanced programming language.

With apologies to Camm, there is one sense in which arriving at ocaml
is neither full circle nor unattractive, and that is the coq theorem
prover.  If there is indeed serious interest in backing Axiom with a
powerful theorem prover, COQ is definitely up there on the list of
candidates.  In fact, some work was done in France a while back on
coq+Axiom - as yet I have not yet located a copy of that thesis,
unfortunately.  I think I posted here about it and got no response. 
Now, before anybody panics let me say I don't think the best option
would be to rely on one prover, any more than I like depending on one
Lisp, and that removes coq+axiom in one image as attractive.  The
reasons for not relying on one prover are also rather more compelling
than the different lisp implementations debate, since these provers
often operate in different styles (guided vs. automatic) and using
different foundational theories.  In an ideal world we would select one
"main" proof engine but be able to work with several others if a user
needed or wanted to.

I know the interest in this topic is spotty, but this is the time and
place to raise the question - if we DO want to be able to back Axiom
with formal provers, what are the design considerations that need to be
taken into account?  What precisely will the prover be used to do, how
would we interact with it, and how would we store and use the results? 
If I'm the only one thinking this way I guess that nominates me to look
into this, but since I have almost no formal training in such matters I
would much prefer to hear from professionals who could make more
definite statements on both the goals and the techniques that would
come into play here.  I'm not proposing to hook a prover into Axiom
right now, or even as part of the Aldor conversion process (although
that would be nice) but I think we should try to define any necessary
logic and/or APIs to enable future use of proof systems in the future. 
I know there has alreay been at least one other effort to study Axiom
with proof logic mentioned here earlier that has its writeup online
(not with coq) so that's probably the place to start.

Cheers,
CY


                
__________________________________ 
Yahoo! Music Unlimited 
Access over 1 million songs. Try it free.
http://music.yahoo.com/unlimited/