[FOM] Object-Oriented Formal Mathematical Languages
spitters at cs.kun.nl
Thu Apr 29 07:27:34 EDT 2004
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
> 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?
More information about the FOM