From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: a07f3367d7,73cb216d191f0fef X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII-7-bit X-Received: by 10.66.121.3 with SMTP id lg3mr2608292pab.41.1364353909319; Tue, 26 Mar 2013 20:11:49 -0700 (PDT) Path: jv11ni187pbb.0!nntp.google.com!npeer01.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!news-in-01.newsfeed.easynews.com!easynews.com!easynews!novia!border4.nntp.dca.giganews.com!border2.nntp.dca.giganews.com!nrc-news.nrc.ca!border3.nntp.dca.giganews.com!border1.nntp.dca.giganews.com!nntp.giganews.com!nx01.iad01.newshosting.com!newshosting.com!news-out.readnews.com!transit3.readnews.com!panix!bloom-beacon.mit.edu!newsswitch.lcs.mit.edu!nntp.TheWorld.com!.POSTED!not-for-mail From: Robert A Duff Newsgroups: comp.lang.ada Subject: Re: Is this expected behavior or not Date: Fri, 22 Mar 2013 19:34:09 -0400 Organization: The World Public Access UNIX, Brookline, MA Message-ID: References: <87ec4b1d-f7cd-49a4-8cff-d44aeb76a1ad@googlegroups.com> <78103a2f-5d19-4378-b211-1917175d5694@googlegroups.com> <3p6p8k0yfly7.ctazdw7fc5so$.dlg@40tude.net> <1jtvzi1v65aqm.1k5ejsveno59f.dlg@40tude.net> <1hvv2kd9smnfx.6spgz9thd1mh$.dlg@40tude.net> <1raubw1sk48ca$.69rdgczvnnf.dlg@40tude.net> <2qwq2cdeuvhu$.qtnb8zyhuob9$.dlg@40tude.net> <39766694-798c-483e-b068-f3f88a00cac4@googlegroups.com> NNTP-Posting-Host: shell01.theworld.com Mime-Version: 1.0 X-Trace: pcls6.std.com 1363995250 23839 192.74.137.71 (22 Mar 2013 23:34:10 GMT) X-Complaints-To: abuse@TheWorld.com NNTP-Posting-Date: Fri, 22 Mar 2013 23:34:10 +0000 (UTC) User-Agent: Gnus/5.1008 (Gnus v5.10.8) Emacs/21.3 (irix) Cancel-Lock: sha1:RqfAV7ETqcsqEupfp+P8KPpi3Do= X-Received-Bytes: 3512 Content-Type: text/plain; charset=us-ascii Date: 2013-03-22T19:34:09-04:00 List-Id: "Dmitry A. Kazakov" writes: > [ It is trivial to put up an example where no compile-time check can exist, > e.g. I don't think so. Compile-time checks just need to be more conservative to avoid running afoul of the halting problem. > function Puzzle return Positive is > begin > if HALT (p) then > return -1; > else > return 1; > end if; > end Puzzle; GNAT has a mode in which the above is a compile-time error. Use the -gnatwae switch, and you are using an Ada-like language in which the above is illegal. It's similar to this Ada: procedure P is Const : constant Integer := 123; begin if HALT (p) then Const := 123; -- Illegal! end if; end Puzzle; The compiler doesn't have to prove that the assignment statement is reachable, nor that the assignment will actually change the value of the constant. It's illegal anyway. The language designer gets to choose between more-conservative compile time rules versus more-liberal run-time checks. > It is a halting problem to prove that Puzzle does not raise > Constraint_Error. ] True, but your first-quoted statement above does not follow from this. In fact, it is trivial to design a language in which all language-defined errors are detected at compile time. (But it's somewhere between difficult and impossible to design a *useful* language with that property.) - Bob