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!nntp-feed.chiark.greenend.org.uk!ewrotcd!reality.xs3.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:11:16 -0500
Organization: Jacob Sparre Andersen Research & Innovation
Message-ID: <mijfqk$nk2$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>
 <migc9a$jp8$1@loke.gir.dk> <miglcs$6gp$1@dont-email.me>
NNTP-Posting-Host: rrsoftware.com
X-Trace: loke.gir.dk 1431126677 24194 24.196.82.226 (8 May 2015 23:11:17 GMT)
X-Complaints-To: news@jacob-sparre.dk
NNTP-Posting-Date: Fri, 8 May 2015 23:11:17 +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: news.eternal-september.org comp.lang.ada:25778
Date: 2015-05-08T18:11:16-05:00
List-Id: <comp.lang.ada>

"Georg Bauhaus" <bauhaus@futureapps.invalid> wrote in message 
news:miglcs$6gp$1@dont-email.me...
> On 07.05.15 20:52, Randy Brukardt wrote:
...
> Why then is the *program* somehow buggy, as you say,
> because some compiler's optimizers can't follow the math that
> has been done already, and expressed as a truth in Pre?

There is no "truth" in Pre; it's just part of the description of the meaning 
of the program. It's madness to assume anything more, you WILL be burned.

And there is little value (IMHO) to separate proofs. At best, you're proving 
what the separate tool *thinks* the semantics should be. Whereas the 
compiler actually *knows* what the semantics are.

Separate tools like SPARK have value today because compilers (and most 
languages!) aren't smart enough to be able to apply proving technology to 
the generation of programs. (Mostly beecause of performance concerns.) But 
that should change over time, and there shouldn't be any reason to keep them 
separate.

It's possible of course that I've reached my expiration date in terms of 
where Ada (and programming languages in general) need to go. Especially as 
most code is mashed-up today and as such is barely functional -- correctness 
is irrelevant when it barely meets any need. But then I (and most of us, in 
fact) have no future (and I worry about the future of humanity as a whole).

                         Randy.