Name: David MENTRE (email_not_shown)
Date: 05/20/04-10:21:40 AM Z


Bertfried Fauser <> 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
( 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
( 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.


[1] I wonder when one french reasearcher will understand the power and
    necessity of free software for real research!

David MENTRE <> --

This archive was generated by hypermail 2b29 : 04/26/17-02:00:02 AM Z CEST