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!news.eternal-september.org!.POSTED!not-for-mail
From: Simon Wright <simon@pushface.org>
Newsgroups: comp.lang.ada
Subject: Re: Ada 2012 Constraints (WRT an Ada IR)
Date: Tue, 06 Dec 2016 09:29:00 +0000
Organization: A noiseless patient Spider
Message-ID: <lyoa0pcso3.fsf@pushface.org>
References: <c06ee4e6-d616-4e01-ba2e-cb111a81f6f6@googlegroups.com>
	<o1kpbo$rni$1@gioia.aioe.org>
	<b777d7e3-4779-4566-b741-8617a9501fd0@googlegroups.com>
	<o1kqk9$tmk$1@gioia.aioe.org>
	<e5adb2c3-f526-4152-9ec9-6e4182e18825@googlegroups.com>
	<o1m2oi$g8l$1@gioia.aioe.org>
	<03847fd7-5699-48de-bb3c-ef5512398f26@googlegroups.com>
	<o1ndod$14ke$1@gioia.aioe.org>
	<3ef819e8-55f7-4ef7-9f37-77e6abc33f98@googlegroups.com>
	<o1oohd$13nu$1@gioia.aioe.org> <o1q81b$9kc$1@franka.jacob-sparre.dk>
	<o1s71b$oi7$1@gioia.aioe.org> <o1sj6s$9vp$1@dont-email.me>
	<o1u6en$1igc$2@gioia.aioe.org> <o1uj70$qe2$1@dont-email.me>
	<o1uroj$jsj$1@gioia.aioe.org>
	<47366b42-c0a3-41bf-a44a-5241c109d60f@googlegroups.com>
	<alpine.DEB.2.20.1612050922450.22845@debian>
	<o23a8a$11e9$1@gioia.aioe.org> <o24om5$vfr$1@franka.jacob-sparre.dk>
	<o24phv$1ou6$1@gioia.aioe.org>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: mx02.eternal-september.org;
 posting-host="864bc9c0338a1658b2b7d47e9713a3a4";
	logging-data="18557"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1/QD1cYLB2698R6ihS1wAy+dlGiESrqLH4="
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.1 (darwin)
Cancel-Lock: sha1:NOuVttpRuPh78hEMx1IsKliz3wA=
	sha1:PfDT8mzJMOvRPjSJHJ5tCQyr7kQ=
Xref: news.eternal-september.org comp.lang.ada:32637
Date: 2016-12-06T09:29:00+00:00
List-Id: <comp.lang.ada>

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:

> On 2016-12-05 23:12, Randy Brukardt wrote:
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>> news:o23a8a$11e9$1@gioia.aioe.org...
>> ...
>>> Things called in Ada pre- and post-conditions if evaluated during
>>> run-time are merely subprogram bodies booby-trapped with
>>> unanticipated exceptions.  Bad thing.
>>
>> Until you compare to the alternative, which is a subprogram body that
>> gives the wrong answer without detection. As I said in another
>> message, a visible bug is much better than an invisible bug.
>
> The alternative is a contract to raise exception. So there is no bug
> anymore, just well-defined behavior.

I'm sorry, but this argument is ridiculous. If I write the code to
implement the required behaviour to the best of my ability, but get it
wrong, then the code will not have the required behaviour and will not
meet any contract that might be placed on it.

The equivalent of your contract would be

   with Post => Correct_Behaviour_Implemented
      or else Something_Terrible_Occurs;

which isn't worth saying.