Damien Doligez wrote:
> On Jul 19, 2005, at 22:14, Robert Morelli wrote:
> 
> 
>> One of the areas where I do much of my programming is in mathematical
>> software.  I view this as one of the most difficult areas,  at the
>> opposite extreme from simple domains like formal methods and language
>> tools.
>>
> 
> Since computer algebra is clearly a subset of formal methods, and a
> pretty good match for OCaml's feature set, I'm rather curious to know
> exactly what kind of mathematical software you are writing, that can
> be so much more complex.

Computer algebra is not all of what mathematical software is about,  and
computer algebra is not,  in practice,  a subset of formal methods.  The
communities of researchers who work in the two fields are traditionally
quite distinct,  with distinct immediate goals,  and the research is
funded and evaluated differently.  For instance,  the NSF in the US
funds several different kinds of computational mathematics research
through several different programs,  and funds formal methods research
through several different programs.

In principle,  the two fields should be merged -- at least in part --
and that is very clearly the vision of some people (though not all).
In practice,  there have been initiatives to bring the two fields
together,  but up until now that has been considered a challenging
interdisciplinary endeavor.

Several years ago I read a paper about a computer algebra system
written in OCaml called FOC.  The title of the paper was something
like "Functors,  blah,  blah,  ... Is it Too Much?"  I think the
conclusion of the paper was that FOC naturally drew upon all of OCaml's
language facilities,  both functional and object oriented.  This paper
might speak to the demands of the domain for anyone who is curious
enough to look it up.  Of course,  we can equally well ask,  "Is it
Enough?"