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=unavailable autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!feeder.eternal-september.org!gandalf.srv.welterde.de!news.jacob-sparre.dk!loke.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail
From: "Randy Brukardt" <randy@rrsoftware.com>
Newsgroups: comp.lang.ada
Subject: Re: {Pre,Post}conditions and side effects
Date: Fri, 8 May 2015 18:31:02 -0500
Organization: Jacob Sparre Andersen Research & Innovation
Message-ID: <mijgvm$tb5$1@loke.gir.dk>
References: <2430252d-52a1-4609-acef-684864e6ca0c@googlegroups.com>
 <AnYlw.957256$Rp.242412@fx23.iad>
 <0a718b39-ebd3-4ab5-912e-f1229679dacc@googlegroups.com>
 <wccoaqucn51.fsf@shell01.TheWorld.com>
 <9ee5e186-5aaa-4d07-9490-0f9fdbb5ca18@googlegroups.com>
 <alpine.CYG.2.11.1412231747100.4196@WIL414CHAPIN.vtc.vsc.edu>
 <wccegrpq2om.fsf@shell01.TheWorld.com>
 <87tww5296f.fsf@adaheads.sparre-andersen.dk> <871tj9dp5b.fsf@theworld.com>
 <ce4af31e-d491-479f-a5b3-0b3eedea2a68@googlegroups.com>
 <midvq5$2u3$1@loke.gir.dk> <mif9j3$ord$1@dont-email.me>
 <1ftovlipftuej.p27p4vog2ka6.dlg@40tude.net> <migb3s$j8q$1@loke.gir.dk>
 <8u3gz9fsuax7$.se3784kmjgvm$.dlg@40tude.net>
NNTP-Posting-Host: rrsoftware.com
X-Trace: loke.gir.dk 1431127862 30053 24.196.82.226 (8 May 2015 23:31:02 GMT)
X-Complaints-To: news@jacob-sparre.dk
NNTP-Posting-Date: Fri, 8 May 2015 23:31:02 +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
Xref: news.eternal-september.org comp.lang.ada:25782
Date: 2015-05-08T18:31:02-05:00
List-Id: <comp.lang.ada>

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:8u3gz9fsuax7$.se3784kmjgvm$.dlg@40tude.net...
> On Thu, 7 May 2015 13:32:28 -0500, Randy Brukardt wrote:
...
>> 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.

That's madness. If the description is sufficiently complete to describe the 
program (and it has to be for the proofs to mean much), then one could have 
generated the program from that description and forget the Ada altogether 
(and most people would do exactly that). And there are few applications 
where there is any value to writing the program twice; for most, it is just 
wasted time. *Especially* if you're adding them after the fact -- what would 
the point be? The program is already debugged and fielded. The only benefit 
to any of these things is in shortening the debugging time, but once that's 
already done, further work is pointless. (We had a rule at RRS about not 
futzing with working code, because we'd been burned by that many times. It 
was necessary to prevent people like me wasting lots of time on "cleanups" 
that ultimately didn't clean up anything. As Tucker likes to say, you can 
move the bump under the rug, but its rare that you can get rid of it.)

                           Randy.