Bertfried Fauser <firstname.lastname@example.org> 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.
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.
 I wonder when one french reasearcher will understand the power and
necessity of free software for real research!
-- David MENTRE <email@example.com> -- http://www.nongnu.org/axiom/
This archive was generated by hypermail 2b29 : 07/25/17-06:40:01 AM Z CEST