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=-0.3 required=5.0 tests=BAYES_00,
	REPLYTO_WITHOUT_TO_CC autolearn=no 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: "G.B." <bauhaus@futureapps.invalid>
Newsgroups: comp.lang.ada
Subject: Re: Ada 2012 Constraints (WRT an Ada IR)
Date: Mon, 5 Dec 2016 20:22:03 +0100
Organization: A noiseless patient Spider
Message-ID: <o24emc$96j$1@dont-email.me>
References: <c06ee4e6-d616-4e01-ba2e-cb111a81f6f6@googlegroups.com>
 <o1jdgk$tja$1@dont-email.me>
 <92ed75e9-baae-455c-9e34-53348dc6eaef@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>
Reply-To: nonlegitur@futureapps.de
Mime-Version: 1.0
Content-Type: text/plain; charset=iso-8859-15; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Mon, 5 Dec 2016 19:20:44 -0000 (UTC)
Injection-Info: mx02.eternal-september.org;
 posting-host="bcd489f2556d3ba711a708fd2cd1fb82";
	logging-data="9427"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1+YEwaa64hEP/v4WbBnEQxWInd2SAjrhK8="
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:45.0)
 Gecko/20100101 Thunderbird/45.5.1
In-Reply-To: <o23a8a$11e9$1@gioia.aioe.org>
Cancel-Lock: sha1:JmhqbzCuKS8PqhEojOmqP3M/IRM=
Xref: news.eternal-september.org comp.lang.ada:32618
Date: 2016-12-05T20:22:03+01:00
List-Id: <comp.lang.ada>

On 05.12.16 09:58, Dmitry A. Kazakov wrote:
> It is either or, never both.

Allow me to consider this statement about assertions as part
of programming as done in general by programmers, assisted by
compilers and such:

  (for all It)[HALT("It is either or, never both.")]

We don't know in general, i.e. not before the fact. Where fact
is proof, or a run-time assertion failing to become true, or
an assumption like some kind of axiom such as "Like the LRM says".

But we can try to express what we think we know, regardless of
whether It is statically true or whether It should be tested
at run-time. At least we can do so until liability is extended
to include perfect functioning of each and every instruction
originating in statements of programs.

-- 
"HOTDOGS ARE NOT BOOKMARKS"
Springfield Elementary teaching staff