Re: A question about Axiom capabilities

 > We did not get time to convert all the comments into code as is done
 > for some the new categories and domains in the trunk repository.
 > For example, from
 >
 > =

http://sourceforge.net/p/open-axiom/code/2800/tree/trunk/src/algebra/catdef=
.spad.pamphlet

Is there a way I could help in a pan-Axiom sort of way? For instance, =

would it be any help if I went through these categories and drew a =

diagram of their relationships? I realise diagrams like:
http://www.axiom-developer.org/axiom-website/bookvol10.2full.html
tend to quickly become unwieldy. But if the diagram was limited to pure =

algebras and split into operator and algebra categories, perhaps it =

might be more manageable?

Or, would it be more practical to model it in one of the formal methods =

tools around, such as?
* Formal specification program,
* Formal development program,
* Formal verification program,
* Theorem provers

I have no experience in using any of these programs but, when they came =

up in this thread I did some searches and they appear to be very =

powerful (I guess their limitations only become clear with experience)?
At first glance CASL appears very powerful for axioms.

quote from wiki page here.
http://en.wikipedia.org/wiki/Specification_language
"In the property-oriented approach to specification (taken e.g. by =

CASL), specifications of programs consist mainly of logical axioms, =

usually in a logical system in which equality has a prominent role, =

describing the properties that the functions are required to satisfy - =

often just by their interrelationship. This is in contrast to so-called =

model-oriented specification in frameworks like VDM and Z, which consist =

of a simple realization of the required behaviour."

So, if I understand correctly:
CASL is good at theories (axiom categories).
ACL2 is good at models of those theories (axiom domains).
(or by Curry=96Howard: proofs)

I have not yet seen a program that is good at both.

I get the impression that ACL2, after a very quick search on the web (so =

I may be wrong), does term rewriting and proofs but its input is not =

axioms but some sort of state machine defined in LISP? (I have not seen =

the light regarding LISP, but let not have that debate!).

So I just wondered if anyone has had experience with any of these =

'formal methods tools' and would there be any benefit in my attempting =

to learn one? (to experiment with specifying axioms or to experiment =

with term rewriting systems).

Or would it be best to wait (hopefully not for the full 30 years) until =

you guys implement more of this stuff?

Martin