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: 103376,ad06d2d7cb045687 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Received: by 10.68.227.40 with SMTP id rx8mr6296065pbc.5.1328326067961; Fri, 03 Feb 2012 19:27:47 -0800 (PST) MIME-Version: 1.0 Path: lh20ni258075pbb.0!nntp.google.com!news2.google.com!goblin2!goblin.stu.neva.ru!newsfeed.x-privat.org!news.jacob-sparre.dk!pnx.dk!jacob-sparre.dk!ada-dk.org!.POSTED!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: Silly and stupid post-condition or not ? Date: Fri, 3 Feb 2012 21:27:40 -0600 Organization: Jacob Sparre Andersen Research & Innovation Message-ID: References: <82wr86fzos.fsf@stephe-leake.org> <5af407fc-2868-44ca-84d2-c51a2a64104d@o4g2000pbc.googlegroups.com> <82k445fu9n.fsf@stephe-leake.org> <143dxzgfasd4o$.a7lekw80xee2$.dlg@40tude.net> NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: munin.nbi.dk 1328326065 26602 69.95.181.76 (4 Feb 2012 03:27:45 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Sat, 4 Feb 2012 03:27:45 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-RFC2646: Format=Flowed; Original X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157 Date: 2012-02-03T21:27:40-06:00 List-Id: "Dmitry A. Kazakov" wrote in message news:143dxzgfasd4o$.a7lekw80xee2$.dlg@40tude.net... > On Thu, 2 Feb 2012 21:13:04 -0600, Randy Brukardt wrote: > >> I've always hated the emphasis on completeness of these things, because >> it >> is *exactly* the wrong approach to getting something in wide-spread use >> (even in the Ada community). > > Putting my hat of logicians on: you can't get anywhere without > completeness. This is how logical inference rules work. Sorry for that, > but > there is no other way. That's complete and utter bunk. As a compiler writer, I know that a compiler can prove all kinds of useful things knowing very little about the program in question. And moreover, any information that the compiler can gain is helpful; it does not have to be complete in any sense. The problem here is that people have allowed themselves to be tied in knots by formal theories, when it's obvious that you can do plenty with nothing but some computing power and a bit of Boolean logic. Formal theories are hardly worth the paper they're written on. Can I prove correctness? No, but that is not now and never will be a useful goal. If it was possible, it would just cause an infinite regress anyway. Specifically, if you can specify the behavior of a program well enough that you can prove 100% of its semantics, then the effort to write the actual program was wasted (at least in the vast majority of programming tasks) -- you would have been better off directly executing the specification. And pretty soon, people will be doing that, and we'll be back to having no proofs of any kind. (And a much harder to understand specification on top of it.) What I can prove is the presence of some bugs and the absence of other behaviors (like raising an exception). And for almost all uses, that's enough. Formal completeness is *always* the wrong goal. Randy.