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 TAA04387 for caml-redistribution; Tue, 31 Aug 1999 19:16:12 +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 SAA20855 for ; Tue, 31 Aug 1999 18:33:26 +0200 (MET DST) Received: from yana.inria.fr (yana.inria.fr [128.93.9.62]) by concorde.inria.fr (8.8.7/8.8.7) with ESMTP id SAA03177; Tue, 31 Aug 1999 18:33:15 +0200 (MET DST) Received: from huet-gera1p (huet-gera2p.inria.fr [128.93.20.113]) by yana.inria.fr (8.8.5/8.8.7) with SMTP id SAA09110; Tue, 31 Aug 1999 18:33:15 +0200 (MET DST) Message-Id: <199908311633.SAA09110@yana.inria.fr> X-Sender: huet@pop-rocq.inria.fr X-Mailer: QUALCOMM Windows Eudora Pro Version 4.0.2 Date: Tue, 31 Aug 1999 18:24:35 +0200 To: Xavier Leroy , Dave Mason , Andreas Rossberg From: Gerard Huet Subject: Re: convincing management to switch to Ocaml Cc: OCAML , John Skaller References: <199908281951.PAA18613@sarg.Ryerson.CA> <37C661C2.D374D8F9@ps.uni-sb.de> <199908281951.PAA18613@sarg.Ryerson.CA> Mime-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable Sender: weis At , Xavier Leroy wrote: >>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 > Yes indeed. It is still a major challenge to write a formal semantics of a non-trivial programming language, with two requirements : 1. It should be reasonably close to an implementation of the language used for real applications 2. It should be machine-manipulable to the extent that at least it brings some confidence about being able to use it to prove some program property or as a basis to a software engineering tool such as a debugger or a static analyser Very very few attempts have been pushed to a convincing stage : - around 1972 Mike Gordon wrote his thesis at U. Edinburgh on a denotational semantics of pure lisp - around 1975 Veronique Donzeau-Gouge wrote her thesis at U. Paris 7 on a denotational semantics of the sequential subset of ADA (which by the way was officially mandatory according to the Stoneman requirements of DoD) - in the early 80's Larry Paulson wrote his thesis at Stanford U. on a semantics of Pascal which was usable at least as an interpreter - in the middle 80's Pierre Weis (yes, the very moderator of this forum!) wrote his thesis at Paris 7 on the Semantic Abstract Machine, implemented it in Caml, and used it to describe fragments of ML and Pascal - in the 80's J Moore wrote what can be considered an executable semantics of an assembler (Python) in the NQTHM prover, and . Boyer attempted various hardware description languages - over the years Peter Moses, Mitchell Wand, Joelle Despeyroux, Frank Pfenning and many others wrote semantics of portions of languages as test examples of meta-description systems - 8 years ago Luca Cardelli and several colleagues from PRL attempted a formal semantics of Modula 3, and even wrote a special PROLOG engine to execute it, but they never saw the end of it and gave up - so today the formal semantics of Standard ML is to my knowledge the sole published complete semantics of a real programming language. I do not believe it answers requirement 2, and probably only a handful of specialists can explain how close it comes to answering requirement 1. Gérard PS Of course 10 years ago it was unconceivable to factor a 512-bits integer, so we can be reasonably sure that one day we shall have a complete semantics of Caml or Java answering both requirements. http://www.inria.fr/Actualites/RSA155.html