Re: {Pre,Post}conditions and side effects

[Georg Bauhaus <bauhaus@futureapps.invalid>]

On 07.05.15 20:52, Randy Brukardt wrote:
> If the compiler fails to optimize the check away, your program is wrong in
> some sense, and you should have gotten an error or warning (depending on the
> compiler mode and exception contracts) to that effect.

With respect, this attitude towards manipulating a program's
meaning during translation makes a compiler assume responsibility
where it really is the programmers' responsibilities (as per
contract), as expressed in clauses like Pre and Post.

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?

As Stefan Lucks explains in his reply, why would a compiler
override what the programmer has stated as a proven truth?
That's not Ada.  That's more like a compiler getting in the way.

I think that

   Pre'__unchecked__ =>

might be in order, then, with the understanding that it's not
real, but conveying the idea.

Thus, if the compiler puts checks where the programmer has
shown they are superfluous, that's not Ada. At least it used
not to be like that.

  "Design your program by obeying our optimizer, be defensive,
   don't bother with logic and proofs! We'll take care.
  "Doing so prevents bugs (if possible)."

That's not Ada. That's another sales strategy.

Are we supposed to forget such contracts entirely because this kind
of formally proven programming is, as you say, not meant by Ada's
new "contracts"?