[FOM] Object-Oriented Formal Mathematical Languages

[Jacques Carette]

Bas Spitters <spitters at cs.kun.nl> wrote:
> 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?

My mistake: when I saw a presentation on Coq, constructivism was emphasized, and the presentation of NuPrl I saw, 
dependent-types were emphasized.  Now that I have looked further into this, you are completely correct that there are 
fewer differences than I believed.  Thank you for the correction.

Moral: when a computer algebra person talks about proof tools, take it with a grain of salt...  

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

FOC does not expose either OCaml nor Coq to the user of the resulting system, although it is exposed somewhat in the 
underlying programming language.  The current system is aimed at computer algebra, and that is where all the published 
theoretical and practical work lies.  While this may well be easily extensible to allow Coq to be exposed, it is not 
implemented as far as I know.

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

You can do constructive reasoning in a classical logic, you just have to be careful about it.  It is true that one 
cannot reliably do automated reasoning in such a system.

However, classical logic is only really hardwired at the level of the meta-theory; currently the framework implies 
that all logics implemented in the system must inherit from the kernel logic - this is being actively discussed for 
modification.  We want to maintain that meta theories use classical logic, but allow theories and logics implemented 
via the system to be constructive.  In fact, since one current application is multi-level programming, we are 
discussing that only the meta-meta-theory be classical.  I like to see this as an idea similar in flavour to the fact 
that the category Cat of all small 1-categories is in fact a 2-category.

Jacques