[Axiom-developer] Questions

[C Y]

I suppose I should know better, but I have a couple "broad scope"
questions about Axiom:

a)  Given the ideal of theoretically backing the mathematics in Axiom
and perhaps even incorporating a proof system into the core design, how
do we handle/document/formalize the interface between "Axiom-level"
code and the underlying lisp functionality?  Ideally, a "provable"
system would be backed by proofs all the way down to the machine code
and chip design levels, but that's well beyond the scope of the Axiom
project.  I'm assuming the point we would want to start using proof
logic is the point where the actual "mathematics" beings, as opposed to
the computational tools and structures needed to support it - is this
correct?  Effectively treat the behavior of the underlying lisp as a
big set of "axioms" (in the mathematical sense) and build off of them?

b)  If we are interested in using Aldor as opposed to Spad for the
"standard" Axiom language, and are forced to re-implement an Aldor
environment due to licensing concerns, would that be the time to build
in proof systems and tools?  Or even if we don't have to redo the
environment - mightn't it still be the time?  Then as we convert things
over to Aldor, document them and prove relevant properties?

c)  I know it's somewhat impractical, but I like the idea of
implementing something once, correctly, documenting it fully, and then
never having to do it again.  Axiom gets closer to that ideal than
virtually any other system I have seen (well, except maybe TeX ;-) and
I think it's one of the great strengths of the program.  I don't know
if unit testing makes much sense for Axiom on the mathematical level
(although perhaps that's what things like CATS are, really) but I can't
help thinking we could benefit if we had some tests which checked for
expected (and depended upon) behaviors from the lisp, OS, windowing
system, or whatever we happen to be depending on.  Ideally, any system
which passed the low level unit tests could properly run Axiom,
although of course more work than that would be needed to rigorously
prove that all answers provided were correct.  Then, if we match those
requirements to things available in the ANSI standard (maybe Paul's
extensive ANSI test suite could provide some ideas for relevant tests
to make), we could claim that it's not our fault if a lisp doesn't
support Axiom ;-)

d)  Tim, assuming I'm not way off base, would it be possible to sort of
define the steps we want to take to get from where we are to the 30
years sytem - e.g. something like:

1) decide on proof system to use, if in fact that's the way we want to
go.
2) integrate proof system with Aldor language and environment
3) outline bootstrapping order in which to document and port systems to
Aldor+Proof Core.
4) As migration occurs, document mathematical theory of all levels and
requirements of Axiom in terms of support from the underlying lisp. 
After a while, with any luck new functionality will be transferred
entirely inside Axiom and the lisp requirements will be clear.

Of course, doing this robustly probably WOULD take 30 years, but then
we would never have to do it again ;-).  I know the more short term
goal is to get the beastie fully working at it's original levels, but
it would be fun to have some broad steps toward the "ideal" Axiom to
start poking around with :-).

Cheers,
CY

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