From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <tom.primozic@gmail.com>
X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr
X-Spam-Level: *
X-Spam-Status: No, score=1.6 required=5.0 tests=AWL,HTML_00_10,HTML_MESSAGE,
	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 93E35BC0A
	for <caml-list@yquem.inria.fr>; Sat,  3 Feb 2007 09:09:07 +0100 (CET)
Received: from nf-out-0910.google.com (nf-out-0910.google.com [64.233.182.188])
	by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l13897Dg023369
	for <caml-list@inria.fr>; Sat, 3 Feb 2007 09:09:07 +0100
Received: by nf-out-0910.google.com with SMTP id m18so1354236nfc
        for <caml-list@inria.fr>; Sat, 03 Feb 2007 00:09:07 -0800 (PST)
DomainKey-Signature: a=rsa-sha1; c=nofws;
        d=gmail.com; s=beta;
        h=received:message-id:date:from:to:subject:cc:in-reply-to:mime-version:content-type:references;
        b=nY1TkNIalhBSP2OMQcG1W1XQgXmSz3mxUfOReyV9Q7tCAOG+eH42YOXO0N4mN34P4m9G1a5BCn5XET6/Zu8zn5WEyQmYYsfz6KktwP+CoeL8XFcx2ZodqwgmHg3pe7J9c+RDR5We0wd7YeUjpQ5FUSqqdEUy/ZFfPMlg68mLHsA=
Received: by 10.82.187.16 with SMTP id k16mr26610buf.1170490146833;
        Sat, 03 Feb 2007 00:09:06 -0800 (PST)
Received: by 10.82.175.13 with HTTP; Sat, 3 Feb 2007 00:09:06 -0800 (PST)
Message-ID: <c1490a380702030009w37582f05s1b146c07e372b15e@mail.gmail.com>
Date: Sat, 3 Feb 2007 09:09:06 +0100
From: Tom <tom.primozic@gmail.com>
To: "Jean-Christophe Filliatre" <filliatr@lri.fr>
Subject: Re: [Caml-list] Programming with correctness guarantees
Cc: oleg@pobox.com, caml-list@inria.fr, Andrej.Bauer@fmf.uni-lj.si
In-Reply-To: <17859.17937.213238.86493@serveur9-10.lri.fr>
MIME-Version: 1.0
Content-Type: multipart/alternative; 
	boundary="----=_Part_48994_10685511.1170490146805"
References: <20070201050431.E278AAB40@Adric.metnet.fnmoc.navy.mil>
	 <17859.17937.213238.86493@serveur9-10.lri.fr>
X-j-chkmail-Score: MSGID : 45C44323.000 on discorde : j-chkmail score : X : 0/20 1 0.000 -> 1
X-Miltered: at discorde with ID 45C44323.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)!
X-Spam: no; 0.00; sml:01 semantics:01 ocaml:01 sml:01 semantics:01 ocaml:01 caml-list:01 programming:03 programming:03 flawed:05 flawed:05 programmer:06 programmer:06 formal:07 formal:07 
X-Attachments: cset="UTF-8" cset="UTF-8" 

------=_Part_48994_10685511.1170490146805
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Content-Disposition: inline

SML is a programming language wit a formal proof of semantics.

I prefer OCaml for it's good implementation - however good a proof, if the
programmer screwed up, or something simply got into way, the end product is
flawed.

Just my two cents...

------=_Part_48994_10685511.1170490146805
Content-Type: text/html; charset=UTF-8
Content-Transfer-Encoding: 7bit
Content-Disposition: inline

SML is a programming language wit a formal proof of semantics. <br><br>I prefer OCaml for it&#39;s good implementation - however good a proof, if the programmer screwed up, or something simply got into way, the end product is flawed. 
<br><br>Just my two cents...<br>

------=_Part_48994_10685511.1170490146805--