RE: [Axiom-developer] Questions

[Page, Bill]

On Thursday, September 15, 2005 3:27 PM C Y wrote:
> 
> I suppose I should know better, but I have a couple "broad
> scope" questions about Axiom:

I really like your questions! I would like to see more
discussions of this kind.

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

Agreed.

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

Yes I think so. To me this means specifically the SPAD and/or
Aldor code from the Axiom algebra library.

> Effectively treat the behavior of the underlying lisp as a
> big set of "axioms" (in the mathematical sense) and build
> off of them?

>From my point of view lisp has very little to do with this
issue. Sorry. :) Consider the fact that the Aldor compiler can
output C code which then gets compiled into machine code by a
C compiler like gcc, just as easily as it can produce lisp code
that either gets interpreted or compiled in turn. To say this
with a positive spin: Lisp is too general and flexible a language
to be well suited to mathematical proofs. A "higher level", i.e.
more semantically constrained and focused language (in the sense
of having a smaller set of more complex primitive operations)
such as SPAD or Aldor, is better suited to expressing mathematical
algorithms nearer the conceptual level at which mathematics
itself is done. Of course this is not a claim that such is not
possible in lisp - it's just that the language (or maybe
sometimes just common practice) does not encourage such usage.

The point is that the "meaning" or semantics of SPAD and Aldor
programs can be specified quite independently of the actually
implementation. Most of this specification of meaning actually
involves known mathematics to a much larger extent then the
usual application of proof techniques to the correctness of
programs in general. I think a claim could be made that
proving that a particular algorithm written in SPAD correctly
implements some specific mathematical result or technique might
be considered formally less difficult (in principle) than
general program correctness because most of the proof can be
carried out at a higher level.

I think you are right that proving the correctness of the
compiler itself or the interpreter needs to be addressed at
a different level. Even within Axiom there are several
intermediate levels, e.g. BOOT code, that could be addressed
separately. Then all the way down to machine code and from
there (in principle) even to the physics. But for *mathematics*
I think (almost) all of the interesting stuff is at the
top of this hierarchy of languages.

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

Personally I think that failure to include Aldor in with Axiom
because of licensing issues would be a minor disaster for both
Axiom and Aldor. I doubt very much that sufficient interested
resources exist anywhere at this point to take on a task like
re-implementing Aldor. Implementing a compiler for a language like
Aldor is already a very BIG job. And imagining adding a program
proof systems on top of that at the same time does not makes much
sense. Also keep in mind that there are a number of very active
projects in this area already such as Haskell, OCaml and OBJ
(to name just a few).

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

Yes, I think that is the right approach! That is exactly where
Tim's ideas about literate program should be the most use.

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

I don't think that is just impractical I think it has been
demonstrated many times over that it is *impossible*! From my
point of view good programming practice these days amounts to
finding ways to do many of the same things over again, in fact
several times over, but to do it efficiently and with (much)
less pain. We need methods for fluently "re-factoring" programs
at a very high level - iteratively re-thinking, documenting and
re-implementing the basic internal design and the relationships
between the components. This is one of the essential tasks of
high level programming language design. I think one of the
fascinating aspects of programming languages like SPAD and Aldor
is that they do in fact seem to facilitate this process.

> Axiom gets closer to that ideal than virtually any other system
> I have seen (well, except maybe TeX ;-)

(: choke, cough :)

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

I think it is much easier to prove "conditional truths",
i.e. proving that the output of a particular algorithm written
in Aldor correctly implements some abstract mathematical
concept ... assuming that the compiler/interpreter and underlying
computer system perform according to spec. Of course this a
weaker result that what the end-user probably desires, but as
far as I can see human intellectual limitations making any
except a level-by-level approach practical.

As I see it "regression testing" is really what Tim's CATS
project can offer - proving that new versions of some package
or module do not produce newly incorrect results which formerly
were deemed to be correct. Or simply showing clearly where the
differences lie. I say "deemed to be correct" because in some
case the lack of formal proofs and the lack of clear and
unambiguous understanding of a problem means that what is
taken to be true at one time *might* change a little over time.

> 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 ;-)

No, I don't think this is the correct view. It is because of
tools like lisp that we can even work at this higher level
at all. We should not be looking to "move the blame" but
rather thinking in terms of building an elaborate and ever
higher scaffolding - sometimes shoring it up underneath and
sometimes building it higher... (: How's that for imagery? :)

> 
> 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 system - e.g. something like:
> 
> 1) decide on proof system to use, if in fact that's the way
> we want to go.

I am very interested to see how Tim will respond to this since
very often we have different views although many of our goals
are the same. :) But I would say emphatically "no" to this. I
think Axiom needs to be open to the application of several
different proof methodologies. (notice my emphasis on the word
*open*).

> 2) integrate proof system with Aldor language and environment

Yes. In fact there has already been some published research
on exactly this topic. Check out some of the articles at
http://page.axiom-developer.org/zope/Plone/refs

> 3) outline bootstrapping order in which to document and port 
> systems to Aldor+Proof Core.

impractical :(

> 4) As migration occurs, document mathematical theory of all levels
> and requirements of Axiom in terms of support from the underlying
> lisp.

Yes. This is very important. It simply must be done if Axiom's
future is to extend to the 30 year horizon.

> After a while, with any luck new functionality will be transferred
> entirely inside Axiom and the lisp requirements will be clear.

No. This does not make sense to me. As I said, lisp has very
little to do with this - except as an intermediate language that
is well-suited to bridging the gap between machine architecture
and high-level complex programming abstractions. It is well suited
primarily because it does not constrain the underlying computational
metaphor. It is like a very high level machine language. But it is
*not* a language that is well suited to expressing high-level
mathematical abstractions - that happens only several levels higher
up.

> 
> Of course, doing this robustly probably WOULD take 30 years, but
> then we would never have to do it again ;-).

I simply do not believe this. If a computer sales person told me
this about some fantastic new computer system, then I think I
would very quickly show him or her the door. :(

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

Finally.... yes indeed. I agree whole heartedly. I think your
project with units of measure and physical dimensions in Axiom
is a very good example. And I like to think of my interest in
category theory in Axiom in the same light.

Regards,
Bill Page.