Re: [Axiom-developer] documentation standards?

[daly]

re: For the future.... (thankfully, a 30 year horizon)

Just so you know, I'm looking at two new, long term efforts, both
of which are invisible if you don't read the source code.



The first effort involves proving Axiom algorithms correct. See Volume 13
which is the long-term place to collect the ideas and practices. This is 
still in the early stages and ideas are still forming around my literature 
readings. Axiom's function signatures really help here.

The primitive change to the source code involves adding things like
loop invariants. For instance, when processing a polynomial you might
see this code:

  while p ^= 0
    ....
    p := reductum p
    ...

Since reductum removes the first term of the polynomial p we know that
the loop will eventually terminate. If we had function properties, we
can automate combining the function property of reductum with the loop
invariant to yield the termination proof, if we had loop invariants.

(It's a form of the old saying 
   "If we had ham we could have ham and eggs, if we had eggs")

I am looking at 3 layers of proof technology. One to move from Spad to
Lisp (Coq?), one to move from Lisp to C (GCL generates C code), and
one to move from C to machine (based on my prior research work on
Intel instruction semantics using Conditional Concurrent Assignments).

I'm also looking at Leslie Lamport's TLA+ language for code decoration. 
It seems to fit our needs reasonably well. 





The second effort is to consider "cost" metrics. Starting from the
ground (Lisp) functions such as +, *, etc. compute a "cost" of a
simple Spad function. Compute the O() cost and decorate the function
with this information.  Find the callers of the function and compute
the O() cost. Recurse.

Ideally this would be computed dynamically so that if a lower level
algorithm is changed it changes the cost of the callers. 

This effort may start to appear in domains such as Integer in the
near future, time permitting.


Tim
(planning to join the NASA Mars team so I can take advantage of
the longer years on Mars.)