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=1.1 required=5.0 tests=AWL,SPF_NEUTRAL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id 7F145BBC1 for ; Wed, 13 Feb 2008 19:27:49 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAALvFskdIDvb1hWdsb2JhbACQQQEBAQgEBQgCCBGWe4YY X-IronPort-AV: E=Sophos;i="4.25,347,1199660400"; d="scan'208";a="22595024" Received: from ag-out-0708.google.com ([72.14.246.245]) by mail4-smtp-sop.national.inria.fr with ESMTP; 13 Feb 2008 19:27:48 +0100 Received: by ag-out-0708.google.com with SMTP id 31so14879827agc.3 for ; Wed, 13 Feb 2008 10:27:47 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:received:received:message-id:date:from:sender:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references:x-google-sender-auth; bh=HVBQNhMb8Rbci1eCtQIe7lNzwUz4yiMUePnqpcQ2dEE=; b=xVPIVPB5gLDn30TxKSrKWmzu1H5Vor7Gl0R4Pay7BuFVFSkjmDE39quap7ZMhnRUQHwMYrKyl35m6cWn1rq3j+KHfsN0vx7QZoA/k6j1ZjKa/rrOgx4+XAzil7MGgApQAUrWuLfC+XNwJJHEfXM/xeZ07GCWBESjfbpbcM73QG4= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:sender:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references:x-google-sender-auth; b=bfF+QKZ3+d30MHMmsWvYa6lLhXsYPiTk5BlTyaCt5vqMzjUsrbfFU6Pxk6P6O0+7A52Gtjgt2o3xvYt5jksGmbRQeIBQMXxpdnMIPpIHrTGuvWypX3DWmAqDQ9+ayTpU/d41g9Sv96wWXkmclinay7W8KZmnFopl2b2Ne6bkLoM= Received: by 10.142.217.17 with SMTP id p17mr208072wfg.139.1202927264770; Wed, 13 Feb 2008 10:27:44 -0800 (PST) Received: by 10.142.148.14 with HTTP; Wed, 13 Feb 2008 10:27:44 -0800 (PST) Message-ID: <4a051d930802131027o6459e7e7i6d35d4eb6e186eea@mail.gmail.com> Date: Wed, 13 Feb 2008 13:27:44 -0500 From: "Christopher L Conway" Sender: christopherleeconway@gmail.com To: "Andrej Bauer" Subject: Re: [Caml-list] Formal specifications of programming languages Cc: caml-list@yquem.inria.fr In-Reply-To: <47B33548.1010001@fmf.uni-lj.si> MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Content-Disposition: inline References: <47B33548.1010001@fmf.uni-lj.si> X-Google-Sender-Auth: e77318f4943d1248 X-Spam: no; 0.00; andrej:01 semantics:01 andrej:01 semantics:01 ocaml:01 coq:01 uniqueness:01 type-checker:01 syntax:01 syntax:01 beginner's:01 ocaml:01 bug:01 preservation:98 beginners:01 But, Andrej, we don't even have an *informal* semantics. :-( You've got to walk before you run. Chris On Feb 13, 2008 1:22 PM, Andrej Bauer wrote: > 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 > > _______________________________________________ > Caml-list mailing list. Subscription management: > http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list > Archives: http://caml.inria.fr > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs > >