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.0 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 mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by yquem.inria.fr (Postfix) with ESMTP id 6C49DBC69 for ; Thu, 4 Oct 2007 20:17:22 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAJ3KBEfAXQImh2dsb2JhbACOOAEBCQon X-IronPort-AV: E=Sophos;i="4.21,231,1188770400"; d="scan'208";a="2147374" Received: from discorde.inria.fr ([192.93.2.38]) by mail1-smtp-roc.national.inria.fr with ESMTP; 04 Oct 2007 20:17:21 +0200 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l94IHLsc004831 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Thu, 4 Oct 2007 20:17:22 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAL/KBEdA6ba9kGdsb2JhbACOOAEBAgcCBiIH X-IronPort-AV: E=Sophos;i="4.21,231,1188770400"; d="scan'208";a="17303075" Received: from nf-out-0910.google.com ([64.233.182.189]) by mail4-smtp-sop.national.inria.fr with ESMTP; 04 Oct 2007 20:17:21 +0200 Received: by nf-out-0910.google.com with SMTP id g13so250234nfb for ; Thu, 04 Oct 2007 11:17:20 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=beta; h=domainkey-signature:received:received:message-id:date:from:user-agent:mime-version:to:subject:references:in-reply-to:content-type:content-transfer-encoding:sender; bh=xnm21pCgos2eKEff8K98rNzLBzf3XcSNH94uaOfW5QU=; b=cI5KTfxuwN2Y5OCh3suC02/2lFb9AFuXtC1l2WurwHl1lwxKd1gR/KJaqS6rHtJF+mvnTcQZWreSN/4tPOwY43seMDxwUWC07M22TjGVOsWSguWqdt3ToDM3BpEwkl4ow0QqTAVPon00yj3scCo4NLdF9YRVSZejN0qLtS6fECs= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:message-id:date:from:user-agent:mime-version:to:subject:references:in-reply-to:content-type:content-transfer-encoding:sender; b=mUR/dHN+G3W4h/y/i0YfO25gqJWIdG5ZXPH5/mssxYWpkQblwHQaVCHKRax4kB7S+hek0KtirjqnP1EGcm2mv/KTSOeaRKPAho9XtsIXxjKrXQYMvzrC0qdSVUYPHBbWkXqCBY7kVP9lPInpTcB+3/ak+vOtynZlWF4MolX05VE= Received: by 10.86.26.11 with SMTP id 11mr1725886fgz.1191521840415; Thu, 04 Oct 2007 11:17:20 -0700 (PDT) Received: from ?192.168.0.5? ( [87.88.165.197]) by mx.google.com with ESMTPS id i5sm3863975mue.2007.10.04.11.17.17 (version=SSLv3 cipher=RC4-MD5); Thu, 04 Oct 2007 11:17:18 -0700 (PDT) Message-ID: <47052E37.8010201@lix.polytechnique.fr> Date: Thu, 04 Oct 2007 20:17:27 +0200 From: Arnaud Spiwack User-Agent: Thunderbird 2.0.0.6 (Windows/20070728) MIME-Version: 1.0 To: caml-list@inria.fr Subject: Re: [Caml-list] Unsoundness is essential References: <20071003083529.40DA2A99F@Adric.metnet.fnmoc.navy.mil> <4703FDEF.7030900@univ-savoie.fr> <1191451810.7218.86.camel@rosella.wigram> <1191462724.7542.76.camel@rosella.wigram> <47049A6D.6020201@univ-savoie.fr> <4704AAA8.9080602@lix.polytechnique.fr> <1191509355.6518.104.camel@rosella.wigram> <470506D9.3080704@fmf.uni-lj.si> <1191515120.6518.173.camel@rosella.wigram> In-Reply-To: <1191515120.6518.173.camel@rosella.wigram> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: Arnaud Spiwack X-Miltered: at discorde with ID 47052E31.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; lix:01 run-time:01 optimistic:98 assertions:01 arnaud:01 arnaud:01 caml-list:01 algorithm:01 data:02 data:02 bugs:03 confused:04 perhaps:05 anyway:05 anyway:05 > Sure, but my point does remain: the expressiveness is more or less > paramount. It is not so much that I personally desire it or not, > but that real programmers in the real world go out there and do > whatever is necessary to make programs work. > That would be wonderful if they did work... Unfortunately to my knowledge, a software is a mere collection of bugs, glued together with a couple of features. Or perhaps I'm being a little optimistic here :p . > A stupid one: how can theoreticians test the efficacy of a new > algorithm with real world case data? > This is obviously not possible (if I understand the question) since real world data don't obey any known law. However they can be modelized for further use. Anyway that is not what you were talking about and I think the discussion got confused due to the wild mix of different notions. One interpretation of what you suggest is to replace pieces of proof by run-time assertions, this sounds a plausible idea, though this is probably not a good thing to do for a finished product. It could however allow the program to be tested before one tries to prove it. There are various other ways to do it, though. Anyway, just be aware that having a more powerful type system usually means much more program that type. Contrary to what you seem to fear. Arnaud Spiwack