Re: convincing management to switch to Ocaml

From: Xavier Leroy (Xavier.Leroy@inria.fr)
Date: Mon Aug 30 1999 - 21:05:00 MET DST


Date: Mon, 30 Aug 1999 21:05:00 +0200
From: Xavier Leroy <Xavier.Leroy@inria.fr>
To: Dave Mason <dmason@sarg.Ryerson.CA>,
Subject: Re: convincing management to switch to Ocaml
In-Reply-To: <199908281951.PAA18613@sarg.Ryerson.CA>; from Dave Mason on Sat, Aug 28, 1999 at 03:51:42PM -0400

> 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



This archive was generated by hypermail 2b29 : Sun Jan 02 2000 - 11:58:24 MET