Re: QED Manifesto and Symbolic Algebra

Eugene Surowitz <[email protected]> Sun, 23 Dec 2018 17:39:01 -0500
Newsgroups gmane.comp.mathematics.axiom.devel
Message-ID <[email protected]>
Tim:

The notion of a "set of measure zero" could just
be hiding the fact that they just don't know what it is ;)

On to something less humorous:

I am about to up grade my primary system to a MAC device
with Windows 10 and Linux as alternate boots.
This is part of a project I've been contemplating
to try to develop a "dual" to AXIOM that would capture the
experience of a "developer" who tries to build a system
from scratch.  "Build" means taking the algebra code
and compiling each component, one by one, until a full
AXIOM system has achieved.

Gene



On 12/22/2018 5:17 PM, Tim Daly wrote:
> 9. Too little care for rigor. It is notoriously easy to find "bugs" in
> algorithms for symbolic
> computation. To make matters worse, these errors are often regarded as
> of no significance
> by their authors, who plead that the result returned is true "except
> on a set of measure
> zero", without explicitly naming the set involved. The careful
> determination, nay, even
> proof, of precisely which conditions under which a result is true is
> essential for building
> the structure of mathematics so that one can depend on it. The QED
> system will support
> the development of symbolic algebra programs in which formal proofs of
> correctness of
> derivations are provided, along with the precise statement of
> conditions under which the
> results are true.
> 
> _______________________________________________
> Axiom-developer mailing list
> [email protected]
> https://lists.nongnu.org/mailman/listinfo/axiom-developer
>