[Axiom-developer] (no subject)

[daly]

> Unfortunately, algorithms not only must be proved 
> mathematically correct, but also be implemented correctly.
>
> There is no fail-safe way to do mathematics other than 
> never leaving any "trivial" or "obvious" claims unchecked, 
> by multiple referees who would have to do the hard work. 
> Nowadays, however, few referees did that. Authors must 
> also accept responsibility for their work.

There is responsibility all the way around.

But if you're going to use a result from Axiom as a step in a proof it
is the role of the Axiom algorithm developer to provide a proof of the
algorithm. And publish the proof so others can reference the proof.

At the moment there is little more than hand-waving, 1800s style. 
"This algorithm implements a commutative function F".  Really?
For all inputs? Or is there a limit to the domain? You used a
function with branch cuts. Which cuts? Does it matter to your
proof? Can you reference the proof of the algorithm you rely upon?

We call this area "computational mathematics" but the emphasis has
been more on the "computational" and less on the "mathematics".

The current state of affairs looks as though we picked up a mathematics 
textbook, copied all of the equations, threw away all the words, and
encrypted the equations in an obscure language.

In my mind, at least, the time has come to "refocus the lens".
Unlike the rest of software, computational mathematics has theory 
behind the algorithms. 

The tools are becoming available (e.g. COQ, ACL2, etc.) to aid proof 
development. The theory exists but is divorced from the code. That was
fine for a "first generation system" like Axiom. But the time has come
for "second generation systems".

It is clear what needs to be done. 
It is clear why it needs to be done.
It is not clear how to do it... which makes it research.
Unfunded research, unfortunately.

At the moment we're in the "stagger around" phase of the research.
Find the papers. Gather a pile. Write a survey. Do an example.
Build a tool. Muscle through a trivial proof. Yaknow, research...

Axiom Volume 13 is the start of the pile. If you find any papers
or articles that might be of interest to the goal, please let me know.

Tim