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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id 52F61BC74 for ; Fri, 5 Oct 2007 00:24:37 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAF8EBUfAXQInemdsb2JhbACOOAEBCQo X-IronPort-AV: E=Sophos;i="4.21,232,1188770400"; d="scan'208";a="2395905" Received: from concorde.inria.fr ([192.93.2.39]) by mail2-smtp-roc.national.inria.fr with ESMTP; 05 Oct 2007 00:24:36 +0200 Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l94MOS8x031012 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Fri, 5 Oct 2007 00:24:36 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAADEFBUdA6ba5kGdsb2JhbACOOAEBAQEHBAQkBw X-IronPort-AV: E=Sophos;i="4.21,232,1188770400"; d="scan'208";a="3770527" Received: from nf-out-0910.google.com ([64.233.182.185]) by mail3-smtp-sop.national.inria.fr with ESMTP; 05 Oct 2007 00:24:36 +0200 Received: by nf-out-0910.google.com with SMTP id g13so311960nfb for ; Thu, 04 Oct 2007 15:24:35 -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=rF7B4jWALYW1T8sjLCADwOap0mMky82Md7CzDDeDX/A=; b=MoZYspfekFusv7chseISTOo8YkdjAQgrkwzqBj4Ux53Vt40Cy+ObvlLO57yyDMzfm6PPP6c+b1ApIc5KOuIXGmEiSXuSKfmvdXI6Kyz4kodpNwZ7x4SJ3NRhR1sKBnxwBli9vsiSpeMnvdr3Uew/J8o4KhmLBpNT3Cd1JYrsNh0= 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=lA9/jnoBkr8HP2TyTMoHn8fILwLevHiXgkSy906KRvbYxVe7PITl+VnljR/OtmX1ZJ8768YN2q2iCrhnnImjZZUI18FAmX370q3Hw061PEu3L4DrEJVV/tmPJ5iX9Br1Pd/MN1f8R0YZCgavSmVCLxAn2f4v8wVG84wSl1eP7PA= Received: by 10.86.4.2 with SMTP id 2mr1895663fgd.1191536673906; Thu, 04 Oct 2007 15:24:33 -0700 (PDT) Received: from ?192.168.0.5? ( [87.88.165.197]) by mx.google.com with ESMTPS id g1sm4318009muf.2007.10.04.15.24.31 (version=SSLv3 cipher=RC4-MD5); Thu, 04 Oct 2007 15:24:32 -0700 (PDT) Message-ID: <47056829.9000602@lix.polytechnique.fr> Date: Fri, 05 Oct 2007 00:24:41 +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> <47052E37.8010201@lix.polytechnique.fr> <1191531254.7078.117.camel@rosella.wigram> In-Reply-To: <1191531254.7078.117.camel@rosella.wigram> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: Arnaud Spiwack X-Miltered: at concorde with ID 4705681C.002 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; lix:01 ocaml:01 toying:01 wiki:01 residual:98 arnaud:01 arnaud:01 caml-list:01 edges:01 expression:02 chalmers:02 programming:03 curses:05 thread:06 probably:07 > In the case of Ocaml, we might say that when many messages > of the form: "This expression has type SquarePeg but is here > used with type RoundHole" have been fixed by sandpapering > off the edges of those pegs .. the program is the residual sawdust > that remains on the floor after thousands of curses. > ^_^ You might really be interested in toying around with interactive systems. I would probably advise Adga2 ( http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php ) or Epigram 1 ( http://www.e-pig.org/ ). Interactive programming tends to save quite a few weird error messages. The type systems of these are of the sort we were discussing on this thread. Arnaud Spiwack