QED Manifesto and Symbolic Algebra

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

QED Manifesto and Symbolic Algebra

Tim Daly
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
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

Re: QED Manifesto and Symbolic Algebra

Eugene Surowtz

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
> [hidden email]
> https://lists.nongnu.org/mailman/listinfo/axiom-developer
>

_______________________________________________
Axiom-developer mailing list
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

Re: QED Manifesto and Symbolic Algebra

Tim Daly
I am rebuilding the Axiom compiler to support the algorihmic
proof technology.  It is a difficult problem and I still have much
to learn. However, I think that we need to connect the "proof"
side of computational mathematics with computer algebra
computational mathematics. After nearly 3 years taking courses
at CMU I think I see how it will succeed.

Whether *I* am capable of doing it is still an open question :-)

Tim

On 12/23/18, Eugene Surowitz <[hidden email]> wrote:

>
> 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
>> [hidden email]
>> https://lists.nongnu.org/mailman/listinfo/axiom-developer
>>
>

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