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.7 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 discorde.inria.fr (discorde.inria.fr [192.93.2.38]) by yquem.inria.fr (Postfix) with ESMTP id 0AE0ABC0A for ; Sun, 10 Dec 2006 20:15:30 +0100 (CET) Received: from py-out-1112.google.com (py-out-1112.google.com [64.233.166.181]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id kBAJFTuF008758 for ; Sun, 10 Dec 2006 20:15:29 +0100 Received: by py-out-1112.google.com with SMTP id b50so790174pyh for ; Sun, 10 Dec 2006 11:15:28 -0800 (PST) DomainKey-Signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=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; b=sh7dt+k74ldlZD/xL11wB+ziyvZ9LhncWMTTXJ3eoqEa3gXZjlEjDoNsKnZxNcgtNjaGy2qiiryYPITwyVSmlACGr705CI6K4ah3KMcGXsRUMiO1BukpEtnqavYX14nkQYaBeZX9wxB631oZpPXDT34tRo6MXb/ZUIUYCaHT3As= Received: by 10.35.75.1 with SMTP id c1mr10680178pyl.1165778128786; Sun, 10 Dec 2006 11:15:28 -0800 (PST) Received: by 10.35.54.6 with HTTP; Sun, 10 Dec 2006 11:15:28 -0800 (PST) Message-ID: Date: Sun, 10 Dec 2006 11:15:28 -0800 From: "Haoyang Wang" Sender: lego395@gmail.com To: "Jean-Christophe Filliatre" Subject: Re: [Caml-list] Today's inflamatory opinion: exceptions are bad Cc: caml-list In-Reply-To: <17788.2858.414320.138285@serveur9-10.lri.fr> MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Content-Disposition: inline References: <004501c71c40$b52e8d00$15b2a8c0@wiko> <17788.2858.414320.138285@serveur9-10.lri.fr> X-Google-Sender-Auth: 63ef43da63ca27f1 X-Miltered: at discorde with ID 457C5CD1.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; erlang:01 o'caml:01 coq:01 coq:01 tactics:98 garbage:01 exception:01 exception:01 caml-list:01 exceptions:01 exceptions:01 caml:02 theorem:02 theorem:02 fails:05 > And regarding exceptions specifically, another of their rules is > this one: > > # Use exceptions only for exceptional situations. For example, when List.find fails to find the item in the list? ;-) Boxing the result in an option type produces more garbage. With automatic memory management, there is less need to clean up after an exception. Thus exceptions can be used quite freely in both Erlang and o'caml. ML was designed for theorem provers, and many of its features can be traced back to that specific purpose. I read somewhere that exception was introduced in ML for back-tracking, which occurs frequently during the normal course of trying out various tactics to prove a theorem. Even today, exceptions are used heavily in coq. Could you comment on your experiences with the usage of caml exceptions in coq? Are exceptions raised there "only for exceptional situations"? Thanks, Haoyang Wang