Re: [Axiom-mail] [open-axiom-devel] A question about Axiom capabilities

[Gabriel Dos Reis]

Martin Baker <address@hidden> writes:

|  > 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?

That would be terrific and greatly appreciated.  It would be beneficial
to lot of people (some of them quietly following the discussion.)

| 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?

Yes.  If you need some tool support, just let me know. 

| 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

Either way, I think your suggestion of drawing relationship between the
fundamental categories is a great one.

On a separate note, I started in 2009 moving in the direction on
integration between OpenAxiom and Isabelle.  The first batch of work led
to initial code generators targetting PolyML (one of the primary ML
implementation used for Isabelle).  Yue was also involved in that
effort.  David Mattews (the main guy behind PolyML) has been very
helpful.  More remain to be done.  

| 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.

Correct.  That is part of the Calculemus project.

| 
| 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!).

ACL2 is a first order prover, the leader in that field; Isabelle/HOl,
Coq are higher order prover, based on lambda calculus encoding.

| 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).

One of the thing we did was to prove that popular object layout
algorithms used by real-world C++ compilers are semantically correct,
and also justify popular C++ programming idioms such as "resource
acquisition is initialization."  See papers here:

   http://www.axiomatics.org/~gdr/formal-cxx/layout-popl11.pdf
   http://www.axiomatics.org/~gdr/formal-cxx/ctor-dtor-popl12.pdf

The work is the subject of a PhD thesis in itself :-)
These things tend work ans scale only when one has a good understanding
of what it is to be implemented -- so having an initial non-formalized
implementation helps a lot.

Xavier Leroy has writen a real world C compiler in Coq:

   http://compcert.inria.fr/

This is a fantastic and colossal work.

| Or would it be best to wait (hopefully not for the full 30 years) until 
| you guys implement more of this stuff?

I am a believer in incremental improvements, so I will take any
improvement you have now :-)

-- Gaby