[FOM] Object-Oriented Formal Mathematical Languages

[Jacques Carette]

Victor Makarov asks:

> Is anyone aware of current work in this direction (design of
object-oriented 
> formal mathematical languages)?

Background: I have spent over 10 years on (and eventually leading) a team
building a commercial Computer Algebra system (Maple, to be precise), and am
now involved in building a 'merged' Computer Algebra system and Proof Tool
[MathScheme].  My main research area is 'foundations' of computer algebra,
especially as it pertains to analysis.  Additionally, I have just finished
teaching a graduate course in programming languages.  I hope this
establishes my credentials for making the comments I make below.

First, it is very important to note that the (current) object-oriented
paradigm is completely inadequate for most mathematics.  This is why you
will find a lot more mathematics being coded in languages that follow a
functional paradigm instead.  The fact that most mathematical objects of
interest need binary (or multi) methods (like addition and multiplication
involving subtyping), dependent types (like matrices) and non-equational
theories (like fields) and so on severely restricts the use of common
object-oriented languages.  This does not seem as well-known as it should
be, but this is nevertheless old knowledge: the writings on Automath of the
late 60s already contain all the ideas necessary to show that weak
programming languages are insufficient.  It is a colossal waste of time to
use OO to try to encode non-trivial mathematics; such a 'prediction' only
reflects the fact that the OO marketers and evangelists are very good at
what they do, and have managed to convince many that OO solves more problems
that it really does.  Even the OO community is slowly starting to realize
the intrisic limitations of their paradigm.  Note: there is currently no one
paradigm sufficient to adequately encode mathematics.

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.

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

Jacques