[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiom-mail] A question about Axiom capabilities, Fwd: [fricas-devel
|
From: |
u1204 |
|
Subject: |
Re: [Axiom-mail] A question about Axiom capabilities, Fwd: [fricas-devel] Abstract Vector Algebra |
|
Date: |
Sat, 06 Apr 2013 00:34:20 -0400 |
>Given that there is no resources (or desire, as far as I can see) to
>change the structure of Axiom
There is the desire. Axiom has a long term goal of introducing
program-proof technology (either COQ or ACL2). ACL2 runs on the same
lisp as Axiom. The plan is to load it into the Axiom image and make it
support program proofs for spad code.
I do not have the resources to attack this problem yet. I am still
rewriting Axiom into literate form. However, I assure you that it
is in Axiom's long-term goals, somewhere in the "30 year horizon".
Look at http://axiom-developer.org (the Axiom home page) and see
item (f), that's the program-proof goal.
Tim Daly