[FOM] Object-Oriented Formal Mathematical Languages

[Bas Spitters]

Hi Jacques,

Jacques Carette wrote:
> On the programming language front, Aldor (http://www.aldor.org) probably
> represents the state of the art in this direction.  Its 'categories' and
> 'domains' (not at all related to either category theory or domain theory)
> are somewhat OO-like, but much better suited to mathematics than traditional
> OO languages.  All of 'algebra' can be very easily and conveniently coded in
> it.
> 
> As far as proof tools go, Mizar (http://mizar.uwb.edu.pl/) certainly has the
> lead on the largest library of formally encoded mathematics.  However,
> NuPRL's type system is much more powerful (http://www.nuprl.org/) [quite
> possibly equivalent to Aldor's], which makes encoding mathematics more
> convenient at times.  It is worth noting that Automath already in 1968 had a
> type system that powerful, but that system was too far ahead of its time.
> Other proof tools (like Coq) are fascinating and powerful, but inadequate
> for classical mathematics because of insistence on constructivism.

I don't understand the distinction you make between Coq and NuPrl. Both 
are based on a constructive type theory and one can, provided one is 
careful, add the principle of excluded middle to both.

What did you mean?

> If one is instead interested in mixing computation and deduction, none of
> the systems above are satisfactory.  The FOC project
> (http://www-spi.lip6.fr/foc/index-en.html) mixes deduction and computation
> for the purposes of building a Computer Algebra system, but does not aim to
> build a proof tool per se. 

The way I understand it is that the FOC system is build "on top" of the 
OCaml programming language and the Coq proof assistant. Thus building a 
new proof assistant for FOC is unnecessary.

> [Shameless plug] The MathScheme project
> (http://imps.mcmaster.ca/mathscheme/) is not quite as far along, but aims to
> build a system where deduction and computation are treated on an equal
> footing, from the basic axiomatization of the system all the way up to the
> user interface.

I was told that classical logic is hardwired in the kernel of the 
MathScheme project, thus making it inadequate for constructive 
reasoning.  Is this correct?

Best regards,

Bas