**Next message:**Camm Maguire: "Re: [Maxima] Re: [Axiom-developer] Re: FeynCalc -> MAXIMA"**Previous message:**root: "Re: [Axiom-developer] FeynCalc -> MAXIMA"**In reply to:**Bertfried Fauser: "RE: [Maxima] Re: [Axiom-developer] Re: FeynCalc -> MAXIMA"**Next in thread:**Richard Fateman: "Re: [Maxima] Re: [Axiom-developer] Re: FeynCalc -> MAXIMA"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]**Mail actions:**[ respond to this message ] [ mail a new topic ]

Hello,

Bertfried Fauser <fauser@spock.physik.uni-konstanz.de> 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 <david.mentre@wanadoo.fr> -- http://www.nongnu.org/axiom/

**Next message:**Camm Maguire: "Re: [Maxima] Re: [Axiom-developer] Re: FeynCalc -> MAXIMA"**Previous message:**root: "Re: [Axiom-developer] FeynCalc -> MAXIMA"**In reply to:**Bertfried Fauser: "RE: [Maxima] Re: [Axiom-developer] Re: FeynCalc -> MAXIMA"**Next in thread:**Richard Fateman: "Re: [Maxima] Re: [Axiom-developer] Re: FeynCalc -> MAXIMA"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]**Mail actions:**[ respond to this message ] [ mail a new topic ]

*
This archive was generated by hypermail 2b29
: 06/23/17-03:40:03 AM Z CEST
*