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: 
 border1.nntp.dca1.giganews.com!nntp.giganews.com!usenet.blueworldhosting.com!feeder01.blueworldhosting.com!feeder.erje.net!1.eu.feeder.erje.net!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:16:27 -0500
Organization: Jacob Sparre Andersen Research & Innovation
Message-ID: <mijg4c$ssi$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> <alpine.DEB.2.11.1505071103310.14859@debian>
 <121ytg16vbxsk$.18dxo1h7daxty.dlg@40tude.net>
 <alpine.DEB.2.11.1505071909280.16448@debian> <migcqf$k21$1@loke.gir.dk>
 <cr1snsF60hoU1@mid.individual.net>
NNTP-Posting-Host: rrsoftware.com
X-Trace: loke.gir.dk 1431126988 29586 24.196.82.226 (8 May 2015 23:16:28 GMT)
X-Complaints-To: news@jacob-sparre.dk
NNTP-Posting-Date: Fri, 8 May 2015 23:16:28 +0000 (UTC)
X-Priority: 3
X-MSMail-Priority: Normal
X-Newsreader: Microsoft Outlook Express 6.00.2900.5931
X-RFC2646: Format=Flowed; Response
X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157
Xref: number.nntp.giganews.com comp.lang.ada:193086
Date: 2015-05-08T18:16:27-05:00
List-Id: <comp.lang.ada>

"Niklas Holsti" <niklas.holsti@tidorum.invalid> wrote in message 
news:cr1snsF60hoU1@mid.individual.net...
> On 15-05-07 22:01 , Randy Brukardt wrote:
>> <Stefan.Lucks@uni-weimar.de> wrote in message
>> news:alpine.DEB.2.11.1505071909280.16448@debian...
>> ...
>>> One property of a proper precondition (or postcondition or ...) is that
>>> disabling the check does not change the functional behaviour of correct
>>> programs.
>>
>> Sure, but this is irrelevant. There are no "correct" programs (in all
>> possible senses). How do you know that you have a correct program? If you
>> use some prover program, it too may have bugs. Or there might be bad data
>> (cosmic rays?)
>
> Those are practical problems, not problems of principle. If you would take 
> the same attitude to mathematics, you would claim that there are no 
> correct theorems. So I disagree with you.

All programming is practical. We do not care about theorems, only that the 
current program is correct in the current environment. Everything has to be 
reproved when anything changes (another good reason for putting it into the 
compiler, as skipping the step isn't possible, and thus problems like the 
Ariene 5 don't happen).

It seems that most of you here are infected with the "theory" disease. I 
want to make practical programming better, and I don't give a damn about any 
stupid theories. Maybe I'm just getting crazy in my late middle age. :-)

                                                  Randy.