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.0 required=5.0 tests=AWL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id 77754BC69 for ; Thu, 4 Oct 2007 03:25:46 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAEPeA0fAXQImh2dsb2JhbACONwEBAQgKJw X-IronPort-AV: E=Sophos;i="4.21,226,1188770400"; d="scan'208";a="17262142" Received: from discorde.inria.fr ([192.93.2.38]) by mail4-smtp-sop.national.inria.fr with ESMTP; 04 Oct 2007 03:25:46 +0200 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l941PNlQ022850 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Thu, 4 Oct 2007 03:25:45 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAMvdA0fLENaMn2dsb2JhbACONwEBAQEHBAYHCBg X-IronPort-AV: E=Sophos;i="4.21,226,1188770400"; d="scan'208";a="2101816" Received: from ipmail01.adl2.internode.on.net ([203.16.214.140]) by mail1-smtp-roc.national.inria.fr with ESMTP; 04 Oct 2007 03:25:43 +0200 X-IronPort-AV: E=Sophos;i="4.21,226,1188743400"; d="scan'208";a="203751690" Received: from ppp121-44-123-220.lns10.syd6.internode.on.net (HELO [192.168.1.201]) ([121.44.123.220]) by ipmail01.adl2.internode.on.net with ESMTP; 04 Oct 2007 10:54:28 +0930 Subject: Re: [Caml-list] Unsoundness is essential From: skaller To: Jacques Carette Cc: caml-list@inria.fr In-Reply-To: <47042202.4070906@mcmaster.ca> References: <20071003083529.40DA2A99F@Adric.metnet.fnmoc.navy.mil> <4703FDEF.7030900@univ-savoie.fr> <1191451810.7218.86.camel@rosella.wigram> <47042202.4070906@mcmaster.ca> Content-Type: text/plain Date: Thu, 04 Oct 2007 11:24:26 +1000 Message-Id: <1191461066.7542.48.camel@rosella.wigram> Mime-Version: 1.0 X-Mailer: Evolution 2.10.1 Content-Transfer-Encoding: 7bit X-Miltered: at discorde with ID 47044103.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; vastly:01 incorrectly:01 int-:01 ocaml:01 type-safety:01 undecidable:01 statically:01 run-time:01 compiler:01 runtime:01 annotations:01 violate:01 run-time:01 assertion:01 type-safety:01 On Wed, 2007-10-03 at 19:13 -0400, Jacques Carette wrote: > skaller wrote: > > To be bold I propose type theorists have got it totally wrong. > > > > Goedel's theorem says that any type system strong enough to > > describe integer programming is necessarily unsound. > > > No, that's wrong. Any *complete* type system that strong is unsound. > It says nothing about incomplete systems. You're right, I have assumed a complete system cannot describe the integer programming. Is that not so? > > I want an unsound type system! > No you don't, you want an incomplete one. You want one where the type > system will tell you when you are obviously wrong, and will ask you for > a proof when it's not sure. If you insist on unsound, then when the > type system doesn't know, it might let things through anyways, and then > all bets are off. I don't want that. Ah, but that is what I *am* arguing for. The 'reasoning' is simply that 'the programmer knows best' -- when the type system doesn't. The evidence is: programming languages with dynamic or unsound typing eg Python, C, are vastly more popular than those with strong typing. Now, my (quite disputable) claim is that the reason for that is that the strong typing people prefer to reject correct programs than accept ones which cannot be proven correct, but this belief is *demonstrably* fallacious. As I demonstrated with simple examples, the type system ALREADY lets incorrectly typed programs through. This fact is hidden by theoretical mumbo-jumbo. It's time the theorists woke up. Leaving out (int-{0}) as a type simply because it would make the type system unsound does not enhance the reliability of the program: either way, without the annotation and a sound type system or with the annotation and an unsound system, it is possible to have a division by 0. The difference is that the unsound system can be improved, and the human brain can do type-checking too. So the unsound system is better because it subsumes the sound one. Nothing is lost in the unsound system. NEITHER system guarantees correctness, and the unsound system still rejects at least the same set of incorrect programs, but possibly more. Ocaml type system is ALREADY unsound: any division by zero or array bounds check exception provides that conclusively. Type systems will NEVER be able to prove all programs are correct. Requiring type safety, i.e. soundness, is simply an obstacle, not an aid. Correctness and type-safety from soundness aren't the same thing. It is better to put more information in the type system, to be more expressive and declarative and accept unsoundness, than to be limited in one's declarative description of executable code, so that in fact the typing is WRONG, in which case the soundness of the type system is of no use in proving correctness! I am arguing in favour of a much richer and more expressive type system, EVEN IF it is not known how to prove type-correctness, and indeed EVEN IF it CAN be proven that there exist cases which are undecidable! > Again, I disagree. It's much better to do most type checks statically, > and then to residualize some type checks to run-time if you absolutely > must. I don't see how I disagree with that. Indeed, that is very much my point! You check what can be checked early, but unless the compiler can PROVE that the code is incorrect, it should not reject it. Unsoundness doesn't imply incorrectness. Any failure caught at runtime by a 'residualised' check proves the type system is unsound. So actually you agree with my point. If indeed the type system were sound there would necessarily not be any need to generate any such run time checks. [Note: this does not mean run time type information isn't required, eg constructor indices, array bounds, etc: run time type calculations subsume mere type-checks] > > In particular, the ability to write proper type annotations > > such as > > > > divide: int * (int - {0}) -> int > > > > and fail to reject programs which violate the typing is an > > essential and useful feature. > I would rather say that what should be done is that run-time type checks > should be residualized into the program, so that no unsound program > would be allowed to run to completion, an assertion would be triggered > first. I told you: you're agreeing with my claim. However it is slightly confused: a program can be correct or not, it cannot be unsound. It is the type system which can be sound or not. So I am going to assume you mean: a program with suspicious typing for which a type-safety proof cannot be found at compile time should have a run time check to ensure the fault consequent of the unsoundness is caught and diagnosed ASAP at run time. I don't dispute the ability to generate such checks is useful, however I raise these issues: 1. What if you cannot generate the checks? 2. Just because the checks pass doesn't mean the program is correct > > In fact, the idea of C is the right one. > When I was forced to write a C program (after enjoying Ocaml so much), > and even with > gcc -W -Wall -Werror -pedantic something.c > I got a clean compile which, when run, core dumped, I was seriously > unhappy. And I got a Not_found error in my Ocaml program recently which took three days to locate. I don't see any qualitative difference. There is a difference of 'degree' which confusingly is a quality issue: better diagnostics, earlier detection, etc. But the bottom line is an uncaught exception in Ocaml and a null pointer dereference in C both cause an abnormal termination symptomatic of an incorrect program (not necessarily due to a typing error). > > Stop CHEATING by refusing to allow > > me to write types you can't check -- because this forces > > ME as the programmer to cheat on the type annotations: > > > > divide: int * int -> int > > hd : 'a list -> 'a > > > Here we agree. Both of those types are 'cheating'. Yes, but your solution might look like this: divide: int * (int \ {0}) -> int with static check on int, and residualised check for a zero divisor .. and for hd, similar... Hey, Ocaml does those checks NOW! SO what's the difference?? The difference is that the system with (int \ {0}) is unsound, but more expressive. My argument is simply that this is BETTER. Not allowing this has no real utility other than to allow theorists to argue the type system is sound. It has no benefits, and many downsides. Perhaps you see a problem where some typing notation is so hard it cannot even be checked at run time? This can surely happen. My answer is: SO WHAT? The programmer is going to code the algorithm ANYHOW. They will either use CHEAT types, in which case the type safety provides no benefit OR, MUCH WORSE .. they're go off and write the program in Python or C instead. -- John Skaller Felix, successor to C++: http://felix.sf.net