[Axiom-developer] Proving Axiom Sane

[Tim Daly]

The idea of proving Axiom "correct" is both too emotionally overloaded

and not quite sufficient to describe the goal.

The goal is similar to compilation but goes far beyond it. Logic demands

that results be "sound" and "complete". Roughly speaking we want to be

sure that we can get results that we can trust. The current forms of logic

relies on "judgements" and rational deductions. Carried to their conclusion

this results in a proof.

But results have various semantics based on the problem and so we

often seek to show that the results are "reasonable", given certain

"provisos".

"Compiling" is not sufficient to cover this breadth of meaning.

Sanity is related to the concepts "reasonable, rational, judicious, sound".

So I'm defining a new term in computational mathematics, "sanity".

To "clean" and "purify" code, to show that it is "sane", run a "sanitizer",
not a "compiler".

The goal is to prove Axiom "sane".

Tim

(whether that term applies to the auhor is questionable)