[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
On formal correctness and readability (was: Re: [Maxima] Re: [Axiom-deve
From: |
David MENTRE |
Subject: |
On formal correctness and readability (was: Re: [Maxima] Re: [Axiom-developer] Re: FeynCalc -> MAXIMA) |
Date: |
Thu, 20 May 2004 10:21:40 +0200 |
User-agent: |
Gnus/5.1006 (Gnus v5.10.6) Emacs/21.3 (gnu/linux) |
Hello,
Bertfried Fauser <address@hidden> writes:
> Hence, for challenging problems, ie new math! and phys!, I would _reject_
> the lates goodies programmers can provide and favour to have a stable, as
> simple as possible, if possible provable algorithm.
This is the path followed by the FOC project
(http://www-calfor.lip6.fr/foc/index-en.html). The objective is to make
a provable CAS. They are using free software for that (the OCaml
language and the Coq proof assistant) but unfortunalty, they have chosen
to make the system closed source and proprietary[1].
On the Axiom side, there is a path that can be followed: using ACL2
(http://www.cs.utexas.edu/users/moore/acl2/) to make a similar
system. Both Axiom and ACL2 (and Maxima) run on GCL. But all the hard
work (i.e. proving things) remain to be done.
> New goodies, may be later added (in a separate pamphlet file <grin>,
> also by people who do not fully understand the theory and purpose of
> the program. They can then check against the slow but stable
> code. This method at least led me to stable and reasonable fast code,
> which at the and was relatively complex.
Interesting idea: systematizing the idea of reference
implementation. And formal proofs between the different implementations
are not necessary. We just need a framework to easily redo a fast
computation with a slower but safer implementation. Of course, formal
proof would be a plus, but I doubt that it can be done.
Yours,
david
[1] I wonder when one french reasearcher will understand the power and
necessity of free software for real research!
--
David MENTRE <address@hidden> -- http://www.nongnu.org/axiom/
- [Axiom-developer] Re: FeynCalc -> MAXIMA, Camm Maguire, 2004/05/18
- Re: [Axiom-developer] Re: FeynCalc -> MAXIMA, root, 2004/05/18
- Re: [Axiom-developer] Re: FeynCalc -> MAXIMA, Bertfried Fauser, 2004/05/19
- Re: [Axiom-developer] Re: FeynCalc -> MAXIMA, root, 2004/05/19
- RE: [Maxima] Re: [Axiom-developer] Re: FeynCalc -> MAXIMA, Stavros Macrakis, 2004/05/19
- Re: [Maxima] Re: [Axiom-developer] Re: FeynCalc -> MAXIMA, Richard Fateman, 2004/05/19
- RE: [Maxima] Re: [Axiom-developer] Re: FeynCalc -> MAXIMA, Bertfried Fauser, 2004/05/19
- On formal correctness and readability (was: Re: [Maxima] Re: [Axiom-developer] Re: FeynCalc -> MAXIMA),
David MENTRE <=
- Re: [Maxima] Re: [Axiom-developer] Re: FeynCalc -> MAXIMA, Bob McElrath, 2004/05/19
- Re: [Maxima] Re: [Axiom-developer] Re: FeynCalc -> MAXIMA, C Y, 2004/05/19
- Re: [Maxima] Re: [Axiom-developer] Re: FeynCalc -> MAXIMA, root, 2004/05/19
- Re: [Maxima] Re: [Axiom-developer] Re: FeynCalc -> MAXIMA, Camm Maguire, 2004/05/23
- Re: [Axiom-developer] Re: FeynCalc -> MAXIMA, Bob McElrath, 2004/05/19
- Re: [Axiom-developer] Re: FeynCalc -> MAXIMA, Bertfried Fauser, 2004/05/19
- Re: [Axiom-developer] Re: FeynCalc -> MAXIMA, Bob McElrath, 2004/05/19
- Re: [Axiom-developer] Re: FeynCalc -> MAXIMA, Camm Maguire, 2004/05/23
- Re: [Axiom-developer] Re: FeynCalc -> MAXIMA, C Y, 2004/05/19
- Re: [Axiom-developer] Re: FeynCalc -> MAXIMA, Camm Maguire, 2004/05/23