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 Path: border1.nntp.dca1.giganews.com!nntp.giganews.com!goblin2!goblin.stu.neva.ru!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: {Pre,Post}conditions and side effects Date: Fri, 8 May 2015 09:50:31 +0200 Organization: cbb software GmbH Message-ID: <8u3gz9fsuax7$.se3784kmjgvm$.dlg@40tude.net> References: <2430252d-52a1-4609-acef-684864e6ca0c@googlegroups.com> <0a718b39-ebd3-4ab5-912e-f1229679dacc@googlegroups.com> <9ee5e186-5aaa-4d07-9490-0f9fdbb5ca18@googlegroups.com> <87tww5296f.fsf@adaheads.sparre-andersen.dk> <871tj9dp5b.fsf@theworld.com> <1ftovlipftuej.p27p4vog2ka6.dlg@40tude.net> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: enOx0b+nfqkc2k+TNpOejg.user.speranza.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit X-Complaints-To: abuse@aioe.org User-Agent: 40tude_Dialog/2.0.15.1 X-Notice: Filtered by postfilter v. 0.8.2 Xref: number.nntp.giganews.com comp.lang.ada:193081 Date: 2015-05-08T09:50:31+02:00 List-Id: On Thu, 7 May 2015 13:32:28 -0500, Randy Brukardt wrote: > "Dmitry A. Kazakov" wrote in message > news:1ftovlipftuej.p27p4vog2ka6.dlg@40tude.net... >> The proof language is another language. It cannot be same language because >> that is inconsistent. > > I completely disagree here. If one is required to write separate proof > instructions, hardly anyone would do it. Still it cannot be the same language. But many, including me, would gladly add proof instructions to critical parts of the program. And this should not preclude sharing same source files for both languages. > After all, developing in Ada > already has a reputation for being slow, doubling that time is never going > anywhere outside of narrow niches. It would meet much more acceptance if adding proof would not be obligatory. I see it as a great advantage too. "Write first, prove later" might sound not much like Ada attitude, but I am sure most programmers will gladly embrace this approach. Most programmers do code cleanup, review, beautification anyway. Adding proofs naturally fits into this phase. > The value of proof, IMHO, is in finding > runtime failures at compile time, both because that will generate better > code, and because earlier detection of errors is better. (This becomes even > more useful in the face of exception contracts, because absence of an > exception is then either proved or the program is illegal.) Yes. > I don't find any value in proving the "correctness" of code (whatever that > means), because the description of what the code does is going to be at > least as complex as the code itself, and thus at least as susptible to > errors. It adds another layer of safety. It also gives another perspective on the program's overall design. Proofs consider the program as a whole with all possible states of, while run time checks and tests deal with only a very small subset of states. > You end up writing the program twice in two different languages. That is the idea. But it is not *the* program. The program is written only once in Ada. The proofs are written *for* this program, they do not change the program itself. Though proofs may hint the programmer to redesign certain parts of the program. > So one language for the majority of us doing "normal" things; perhaps two > languages for extreme cases (but I'm not remotely interested in that - > thinks like SPARK are terribly limiting). That is because of all or nothing attitude. Proofs must be really optional. They should not be required in upfront design. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de