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=-0.3 required=5.0 tests=BAYES_00, REPLYTO_WITHOUT_TO_CC autolearn=no 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.226.10 with SMTP id ro10mr6875505pbc.6.1328350547866; Sat, 04 Feb 2012 02:15:47 -0800 (PST) Path: lh20ni259118pbb.0!nntp.google.com!news2.google.com!news3.google.com!proxad.net!feeder1-2.proxad.net!usenet-fr.net!gegeweb.org!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: Silly and stupid post-condition or not ? Date: Sat, 4 Feb 2012 11:15:37 +0100 Organization: cbb software GmbH 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> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: uPp0VmqFNQ7upgD/pR45FA.user.speranza.aioe.org Mime-Version: 1.0 X-Complaints-To: abuse@aioe.org User-Agent: 40tude_Dialog/2.0.15.1 X-Notice: Filtered by postfilter v. 0.8.2 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Date: 2012-02-04T11:15:37+01:00 List-Id: On Fri, 3 Feb 2012 21:27:40 -0600, Randy Brukardt wrote: > "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. No, you don't need all information, but each piece you get must be complete in itself. Informally, completeness is just about knowing the choices to make. > 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. Quite so, but there still exist hard facts, which cannot be ignored without being punished. 2x2=4, function is not a constructor (:-)) > Can I prove correctness? No, but that is not now and never will be a useful > goal. I don't think so. As the amount and complexity of the software grows the traditional means of ensuring software quality stop working both technically and economically. I see it on the example of GNAT compiler. Probably most experienced and talented people in the world cannot get it right for about 20 years. 20 years is the age of one generation. > If it was possible, it would just cause an infinite regress anyway. True. You always need to take some things for granted. That is no problem to me. This seems to be a problem to people from your camp: we cannot check for Strorage_Error! Why? Of course you can, just let the programmer fill the gaps, let proofs be conditionals. Any proof is conditional because of that infinite regress. Why throwing everything away? > 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.) And again, this is what you get. If you refuse to integrate formal stuff into the language, then, inevitably, an ugly modeling tool to come. And one uglier on top of it and so on. Tools prey and feed on weak languages. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de