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 Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer
