From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id OAA14572 for caml-redistribution; Tue, 31 Aug 1999 14:16:43 +0200 (MET DST) Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id VAA07668 for ; Mon, 30 Aug 1999 21:05:12 +0200 (MET DST) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.8.7/8.8.7) with ESMTP id VAA29496; Mon, 30 Aug 1999 21:05:02 +0200 (MET DST) Received: (from xleroy@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id VAA25450; Mon, 30 Aug 1999 21:05:00 +0200 (MET DST) Message-ID: <19990830210500.37195@pauillac.inria.fr> Date: Mon, 30 Aug 1999 21:05:00 +0200 From: Xavier Leroy To: Dave Mason , Andreas Rossberg Cc: OCAML , John Skaller Subject: Re: convincing management to switch to Ocaml References: <37C661C2.D374D8F9@ps.uni-sb.de> <199908281951.PAA18613@sarg.Ryerson.CA> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Mailer: Mutt 0.89.1 In-Reply-To: <199908281951.PAA18613@sarg.Ryerson.CA>; from Dave Mason on Sat, Aug 28, 1999 at 03:51:42PM -0400 Sender: weis > 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