Re: convincing management to switch to Ocaml

[Gerard Huet <Gerard.Huet@inria.fr>]

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