From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=AWL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id 32682BBC1 for ; Wed, 13 Feb 2008 19:20:27 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAN/DskfBAkMth2dsb2JhbACQQQEBAQgKKZ0A X-IronPort-AV: E=Sophos;i="4.25,347,1199660400"; d="scan'208";a="9153220" Received: from vega.fmf.uni-lj.si (HELO postar.fmf.uni-lj.si) ([193.2.67.45]) by mail3-smtp-sop.national.inria.fr with ESMTP; 13 Feb 2008 19:20:26 +0100 Received: from localhost (unknown [192.168.5.1]) by postar.fmf.uni-lj.si (Postfix) with ESMTP id 1230D32F581 for ; Wed, 13 Feb 2008 19:20:26 +0100 (CET) X-Virus-Scanned: amavisd-new at spam.fmf.uni-lj.si Received: from postar.fmf.uni-lj.si ([192.168.5.5]) by localhost (spam.fmf.uni-lj.si [192.168.5.1]) (amavisd-new, port 10024) with ESMTP id 9-7D+37uiMdJ for ; Wed, 13 Feb 2008 19:20:25 +0100 (CET) Received: from [192.168.1.113] (BSN-77-148-136.static.dsl.siol.net [193.77.148.136]) (Authenticated sender: bauer) by postar.fmf.uni-lj.si (Postfix) with ESMTP id AB66932F578 for ; Wed, 13 Feb 2008 19:20:25 +0100 (CET) Message-ID: <47B33548.1010001@fmf.uni-lj.si> Date: Wed, 13 Feb 2008 19:22:00 +0100 From: Andrej Bauer User-Agent: Thunderbird 1.5.0.14pre (X11/20071023) MIME-Version: 1.0 To: caml-list@yquem.inria.fr Subject: Formal specifications of programming languages Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit X-Spam: no; 0.00; andrej:01 andrej:01 semantics:01 semantics:01 ocaml:01 coq:01 uniqueness:01 type-checker:01 syntax:01 syntax:01 preservation:98 typing:01 typing:01 proofs:01 formalism:01 I see people have opinions about formal semantics. Having formal semantics for a programming language is a valuable thing, even if most people do not understand it. Such semantics is a piece of mathematics that removes (hopefully) every doubt as to what we are talking about, and has other benefits as well. High priests can then write sermons in common language and explain the meaning of the Holy Word. It would probably be quite hard to provide formal semantics for complete ocaml, for several reasons, such as sheer size, C interface, and the fact that it is a moving target. But what is formal semantics good for? Complete formal semantics written with a tool such as Coq, together with formal proofs of its properties (existence of principal types, uniqueness of typing, type preservation, progress lemma) is good for automatic extraction of a prototype type-checker and/or interpreter. This can be extremely valuable for PL researchers who want to experiment with new features. Incomplete formal semantics written in a series of papers and dissertations is still quite useful. It allows researchers to clearly express and communicate ideas. Once a person learns how to read the mathematics that may greatly help his or her understanding of corner cases and peculiar examples. We (researchers) should encourage "ordinary programmers" to read formal semantics by writing manuals and textbooks that incorporate the formalism and decorate it with sufficient explanation. Think about the fact that specifying concrete syntax in BNF-like formalism has become the norm. Programmers happily read it and the benefits are obvious. Nobody suggests that syntax should be explained in English prose because BNF is too hard to understand. So why are you suggesting that the norm for describing other pieces of a programming language, such as typing rules and operational semantics, should be primarily (or only) English prose? Andrej