Re: convincing management to switch to Ocaml

[Xavier Leroy <Xavier.Leroy@inria.fr>]

> Would it really be beyond a Master's student working under Xavier (or
> other CAML guru) to translate the SML formal spec into a CAML formal
> spec?  Or at least a PhD student.

It's not just a translation.  Some of the features of OCaml (such as
the recursive object types, the partially unspecified evaluation
order, and the whole class system) have deep impact on the formal
semantics and would require a total rewrite.

More generally, don't underestimate the difficulty of producing a
formal definition of a real-world language.  The "Definition of
Standard ML" wasn't written by one student, but by one Turing award
recipient and two world-class specialists in type theory and
operational semantics, and I believe it took them well over one year.

The issue of writing a formal definition of OCaml has been discussed a
lot here at INRIA in projet Cristal, and the consensus is that it's
well over our manpower.  My opinion on this is that it's hopeless
without machine assistance to write, type-check, execute on small
examples, and perhaps even prove basic properties of the spec.  None
of the existing tools in this area (e.g. Centaur, Coq, ELF,
lambda-Prolog) seem adequate for this task, and while there's some
promising work in progress in this direction, it's still very much an open
research problem in itself.

- Xavier Leroy