Re: [Axiom-developer] Aldor and Lisp

[C Y]

--- Camm Maguire <address@hidden> wrote:

> Greetings, and thank you for this initiative!

Second that!
 
> If someone can concisely specify exactly what is missing in SPAD vis
> a vis Aldor, it would be most helpful.  What are these most 
> remarkable features?  Examples?  Alas, I lack time to plough through 
> the 300 page aldor manual.

Agree there, unfortunately.  As soon as we decide definitely on Aldor
either due to its finally being released or updating/modernizing our
own SPAD code to become a new Aldor implementation I'll have to go
through it, but currently I'm still trying to figure out dimensionless
dimensions and other fun.  I guess I'm kinda hoping that by the time I
finally get this well enough to try any actual coding the decision as
to which path to take will have been made and progress begun.

> Just my 2 cents here -- it really doesn't matter what tool we use, as
> long as it is open source and we can get mind-share circled around
> its development.  I know this first hand in working with GCL from 
> scratch knowing no lisp at all. Once one decides to invest in the 
> learning curve, the very last thing we should do is flip flop -- 
> expertise is the value we supply and it takes time and is hard to 
> come by.

Bingo.  Another reason I'm not really worried about coding yet - I do
NOT want to figure out SPAD only to have to redo everything again in
Aldor.  At the level of exactitude of mathematical programming, I'm not
sure there is really such thing as a minor difference in languages.  A
mathematical proof failing for a "minor" reason as opposed to a "major"
one still fails, and the same could be said for a slightly
mistranslated Axiom program.

> Given where the cards appear to lay right now, extending/fixing 
> SPAD to match Aldor appears the obvious choice.  

I know Bill is concerned about the amount of work that would take, and
I agree with him, but I agree - open source comes above any convenience
gained by using a closed source Aldor.  One Macsyma Inc. is enough - we
don't want to depend on ANY closed source technology, at any level.  

The other point is that we don't want to wait indefinitely trying to
free up Aldor as it currently stands, or we will lose momentum.

> I am assuming a lot here, but it is primarily that the factors 
> behind the Aldor rewrite decision went something like 1) this code 
> has cruft, time for a rewrite 2) we're in the AI winter, nobody uses
> lisp anymore, and its slow, 2.5) its more fun and easier to start 
> over than try to understand and build upon the work of others, even 
> if it does effectively destroy the value of everyone's time spent on 
> the older stuff, 3) lets build something totally new in C.  These 
> motivations are not commensurate with those we face in the open 
> source world.  I'm also assuming that Aldor is basically like spad 
> but nicer, faster, and a little more powerful.  If I'm missing 
> something as is quite likely, the conclusion obviously does not hold.

Heh - I would be sorry to lose the potential underlying flexibility and
power of lisp.  Axiom's mathematical power might reside in
SPAD/Aldor/Whatever but having lisp underneath it could have some real
advantages.  (Yes, I'll admit my bias - I still think the lisp gui
toolkits could be used to make an out of this world Mathematics GUI
someday.) 

> Here too, it is a complete waste of time, IMHO, trying to make sure
> axiom or any system runs on 11 different compilers.  Choose one,
> establish the expertise needed to ensure that it will remain
> servicable for the indefinite future, and then concentrate on adding
> functionality to AXIOM.  

The problem there, Camm, is that there is no way to ensure ANYTHING
will remain servicable for the indefinite future.  Where would GCL be
without you, for example?

The way I would prefer to say it (which you might agree with) is that
Axiom should target running as much as possible on ANSI Common Lisp as
defined in the standard, and GCL (which is also striving to reach the
goal of being ANSI) should remain its primary development platform. 
(At least for a while - there is one direction I would like to see
things head that I doubt GCL could support, but its so speculative it's
not worth worrying about now.) If both achieve the ANSI goal, then
other standards compliant lisps should also have no trouble with Axiom
as a bonus.  But being standards compliant is the key. 
 
> I've been having a lot of correspondence lately with theorem-prover
> authors, and I've come to appreciate Tim's original idea of using one
> to verify AXIOM.  Having something like this would clearly put AXIOM
> at the head of the pack IMHO.

I have also been looking at this a little, and I agree fully.  I think
that if (when?) we finally decide Axiom will become fully based on
Aldor, we should also at that time incorporate methods for
incorporating whatever features are necessary or desirable for
interacting with theorem provers.  Here I think, unlike the lisp issue,
that it is important to be flexible with what is possible because
provers differ from each other not only in implementation but kind.  It
needs looking at, but I also agree that this could be an honest to
goodness "killer feature" that puts Axiom on the map in a very, very
big way.  But if we're going to be rewriting over into Aldor anyway, we
should also put the full power of everything modern proof software can
bring to bear into the mix.

Actually Camm, do you know anything about proving compilers? (I know
it's a different problem from the mathematical proof question, but not
as much as one might think - after all, the correct execution of every
mathematical Aldor/SPAD statement depends on the correct functioning of
all support software.)  I don't expect us to be able to write a
provable compiler, but I would like us to design things in such a way
that they would be amenible to future proof efforts.  For example, have
each element of the Aldor language state properties it relies on, and
have the compiler (or maybe translater/parser?) that goes from Aldor ->
Lisp might someday verify properties requested are true in the lisp
structure built?  I suppose this would require an explicit statement of
a lot of stuff lisp doesn't usually make explicit though.

I've been thinking about this some - mathematicians are very reluctant
to accept the idea of computers as useful or reliable tools in matters
such as proofs, and given the behavior of modern software its a bit
hard to blame them.  I think something like the following the only way
the diehards will ever come around:

a)  Axiom and similar pieces of software are capable of constructing
proof arguments for any and all mathematical outputs.
b)  Automatic provers can verify the proof, based on already proven
libraries or verification of supplied logic (or auto-generated
arguments if that type of prover is mature enough to be useful)
c)  provers are programmed using modern provable software techniques
(the B method, Z, VMD, bitc, what have you)
d)  provers are compiled to machine code by compilers also verified
with proof techniques
e)  assembly language, machine language, and hardware designs are also
subject to proof of advertized properties.  In the case of hardware,
probability of error calculations are the root truth of the situation,
so the probability of any possible error or sequence of errors is
always nonzero, but since the same thing may be said for the human
brain and there it is impossible to quantify...

Of course, at some point in the basic design human beings have to
verify and certify proofs to avoid circularity, but I think that point
should be well defined and as close to minimum as possible.  

Some of the steps might be wrong or I might have missed some, but I
think eventually the entire software and hardware stack of a proof
system will have to be subject to formal methods and formal proofs,
insofar as that is possible.  But I am not convinced the human brain
has any fundamental advantage over a computer when it comes to
verifying proofs are correct, and I think the maximum obtainable
certainty with a proof verified by a maximally verified computer will
be greater than that obtainable from human examination, particularly as
proof complexity grows.  

Of course, I don't propose the Axiom project tackle all this - it's far
beyond the scope of the project.  However, I would like to see things
written to allow a) use of current, already useful tools and b) be
ready should the opportunity arise to fit Axiom and Aldor on top of a
proven software and hardware stack.


> > Of course, the current compiler and interpreter for Axiom's
> > extension language ("spad"), is written in a dialect of lisp 
> > (called "boot"), which itself is written in lisp.

If I may ask, how come the boot step is needed?  Do we need it in the
Aldor -> Lisp translation?  I understand the need to limit the power of
Lisp in Aldor (if I understand correctly we actually don't WANT to
express mathematics in a turing complete language because of the
undecidability of various problems in such an environment?) but surely
it is possible to write code in Lisp itself to generate logical
structures with the necessary properties without having to define a
secondary "boot" language?  (I confess here I'm thinking of the
undesirability of proving the Aldor -> boot step as well as the boot ->
Lisp step in the future.)  Tim Daly wrote a summary of the languages in
Axiom some time ago, I'll have to go dig it up and read it again.

Cheers,
CY


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