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=none autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id 3FA04BBC1 for ; Sun, 27 Apr 2008 16:20:09 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: An0AAPYnFEhQW+UCmmdsb2JhbACRWgEBAQEBCAUIBxEElxA X-IronPort-AV: E=Sophos;i="4.25,712,1199660400"; d="scan'208";a="10129473" Received: from concorde.inria.fr ([192.93.2.39]) by mail2-smtp-roc.national.inria.fr with ESMTP; 27 Apr 2008 16:20:09 +0200 Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id m3REK66G003731 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Sun, 27 Apr 2008 16:20:09 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: An0AAPYnFEhQW+UCmmdsb2JhbACRWgEBAQEBCAUIBxEElxA X-IronPort-AV: E=Sophos;i="4.25,712,1199660400"; d="scan'208";a="10129472" Received: from main.gmane.org (HELO ciao.gmane.org) ([80.91.229.2]) by mail2-smtp-roc.national.inria.fr with ESMTP; 27 Apr 2008 16:20:06 +0200 Received: from root by ciao.gmane.org with local (Exim 4.43) id 1Jq7jW-0000TE-Gk for caml-list@inria.fr; Sun, 27 Apr 2008 14:20:02 +0000 Received: from cpe-74-73-3-62.nyc.res.rr.com ([74.73.3.62]) by main.gmane.org with esmtp (Gmexim 0.1 (Debian)) id 1AlnuQ-0007hv-00 for ; Sun, 27 Apr 2008 14:20:02 +0000 Received: from cconway by cpe-74-73-3-62.nyc.res.rr.com with local (Gmexim 0.1 (Debian)) id 1AlnuQ-0007hv-00 for ; Sun, 27 Apr 2008 14:20:02 +0000 X-Injected-Via-Gmane: http://gmane.org/ To: caml-list@inria.fr From: Christopher L Conway Subject: Re: [OSR] Standard syntax extensions ? Date: Sun, 27 Apr 2008 14:14:37 +0000 (UTC) Message-ID: References: <1209052182.6180.35.camel@Blefuscu> <74cabd9e0804251337m40811532yb359710630cdbdfd@mail.gmail.com> <20080426074157.GA15640@annexia.org> <74cabd9e0804261432o116f4db5w2f5777496da17d94@mail.gmail.com> <48142430.9000705@andrej.com> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Complaints-To: usenet@ger.gmane.org X-Gmane-NNTP-Posting-Host: main.gmane.org User-Agent: Loom/3.14 (http://gmane.org/) X-Loom-IP: 74.73.3.62 (Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9b5) Gecko/2008041514 Firefox/3.0b5) Sender: news X-Miltered: at concorde with ID 48148B96.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; syntax:01 andrej:01 andrej:01 infix:01 syntax:01 corresponds:01 notation:01 notation:01 type-safe:01 semantics:01 skipping:01 misused:98 wrote:01 clearer:01 proofs:01 Andrej Bauer andrej.com> writes: > Arthur Chan wrote: > > That > > said, there are some of us who feel that that the python infix syntax is > > clearer, and as it corresponds more directly to the mathematical > > notation, it is just as provably correct as the List.mem notation is. > > If reusing "in" is a big deal, then maybe we could do "in_list" or > > "inlist"? That'd be more type-safe too. > > Just a small correction, if you will alow me. When we speak of > correctness of a programming language we do not say that "syntax is > provably correct" but rather that the "implementation is correct". I think what Arthur meant by "provably correct" was "has well-defined semantics, aiding proofs of correctness." > Actually, the whole phrase "provably correct" is often misused in > computer science, at least the way I understand it. If you prove > something then it is "proved correct", while a thing is "provably > correct" if we _could_ prove it correct. Perhaps a native speaker of > English can clarify this point. You have a point, from a prescriptive point of view. But in the common usage "provable" and "proved" are sometimes interchanged. Most computer scientists aren't Platonists: "provable" means "I could describe the proof for you, step by step, if you like, but let's save some time by skipping it." Saying a claim is "provable" without working out the proof begs the question. > Isn't everything on this list a minor quibble? Happy quibbling, Chris