Proving Axiom Sane

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
1 message Options
Reply | Threaded
Open this post in threaded view
|

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)




_______________________________________________
Axiom-developer mailing list
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer