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.5 required=5.0 tests=SPF_SOFTFAIL autolearn=disabled version=3.1.3 Received: from discorde.inria.fr (discorde.inria.fr [192.93.2.38]) by yquem.inria.fr (Postfix) with ESMTP id 8F1DDBC0A for ; Fri, 22 Dec 2006 21:03:20 +0100 (CET) Received: from mail.davidb.org (mail.davidb.org [66.93.32.219]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id kBMK3If2011681 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO) for ; Fri, 22 Dec 2006 21:03:20 +0100 Received: from a64.davidb.org ([66.93.32.226]) by mail.davidb.org with esmtpa (Exim 4.62 #1 (Debian)) id 1Gxqbm-0006rP-Hr; Fri, 22 Dec 2006 12:03:10 -0800 Message-ID: <458C39FD.7090409@davidb.org> Date: Fri, 22 Dec 2006 12:03:09 -0800 From: David Brown User-Agent: Thunderbird 1.5.0.8 (X11/20061111) MIME-Version: 1.0 To: skaller Cc: =?UTF-8?B?RGFuaWVsIELDvG56bGk=?= , caml-list@yquem.inria.fr Subject: Re: strong/weak typing terminology (was Re: [Caml-list] Scripting in ocaml) References: <6dbd4d000612201941wcd4b09anc503a13889576512@mail.gmail.com> <20061221153413.8f99e8ed.mle+ocaml@mega-nerd.com> <1166685756.5337.4.camel@rosella.wigram> <458A8C7B.7050204@hq.idt.net> <1166709162.5653.11.camel@rosella.wigram> <458AA143.3090303@hq.idt.net> <20061221202520.GG9440@apotheon.com> <20061221221650.GL9440@apotheon.com> <3EC73FC3-41A6-4FB1-9549-29286A6568CC@epfl.ch> <1166811403.6555.46.camel@rosella.wigram> <4E1EAAC5-DC08-4A55-9AEB-0D5D3BE1C0EA@epfl.ch> <1166816522.7448.45.camel@rosella.wigram> In-Reply-To: <1166816522.7448.45.camel@rosella.wigram> Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit X-Miltered: at discorde with ID 458C3A06.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; ocaml:01 dumped:01 restrictive:01 compiler:01 statically:01 runtime:01 wrote:01 typing:01 exception:01 caml-list:01 caml-list:01 constraint:01 data:02 instances:02 subsets:02 skaller wrote: > This is not my understanding of what safe means. > Your program is safe? Ok, so would you use it to > control a nuclear reactor? Do you really think anyone > cares if the reactor blows, whether the program > core dumped, failed to core dump, or threw an exception? > > to me safe means 'cannot fail'. But perhaps i misunderstand: > it would be interesting to see another definition. This is certainly a good definition of "safety", but not one commonly used when referring to type systems. It also has problems with undecidability, and trying to enforce it generally results in programming languages or language subsets that are so restrictive that general purpose programming becomes very tedius, or just impossible. Even systems that put a lot of effort into this kind of safety (such as SPARKAda) don't claim that they "cannot fail", but instead refer to it as high-integrity. Most references use phrases like "type safety", although this seems to get different definitions depending on the user. Although specific instances in a program, the compiler might be able to statically determine if an array bounds is going to be violated, this can't be done in the general case. So, I'm not sure how defining "safe" so high that it can't be implemented is useful to anyone. Those interested in this topic should definitely read up on the Ariane 5 rocket's first launch. For efficiency considerations the developers disabled some of the runtime constraint checks on data conversions, which resulted in this failure. Dave