Re: [Axiom-mail] A question about Axiom capabilities

[Martin Baker]

> 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–Howard: 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