[Aldor-l] Re: Specifying properties of functions

[Manuel Bronstein]

> > [ MB: ]
> > There have been projects to mix axiom and aldor with theorem
> > provers so that one could indeed write axioms satisfied by the operations
> > in the categories themselves (ie x*y=y*x for all x,y in CommutativeRing).
> > They required compiler changes, and while they were mathematically elegant,
> > it is unclear that there was a gain in expressiveness for the programmers.
> 
> [ RH: ]
> I also don't see yet, how such axioms could help the _programmer_ much.
> The point is that in Aldor the properties are given through the 
> documentation (like for CommutativeRing) but not by a formal 
> description. And yes, you guessed rightly that the final goal should be 
> to put Aldor also into the frame of automated theorem proving. But maybe 
> that is a very long term goal...
> 
> Can you give some references to these axiom/aldor/theorem prover projects.

For putting properties into the aldor type systems, check out the Atypical
project home page at  http://www.cs.kent.ac.uk/people/staff/sjt/Atypical/
This is the most relevant to what is being discussed in this thread.

An earlier project mixing axiom (sorry, not aldor) and NuPRL is described 
at  http://www.nuprl.org/documents/Constable/towardsintegrated.html

-- mb