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!.POSTED!not-for-mail
From: Simon Wright <simon@pushface.org>
Newsgroups: comp.lang.ada
Subject: Re: How to get Ada to ?cross the chasm??
Date: Thu, 10 May 2018 20:36:04 +0100
Organization: A noiseless patient Spider
Message-ID: <lyzi17fgm3.fsf@pushface.org>
References: <322f9b26-01de-4753-bb50-6ef2f3d993d8@googlegroups.com>
	<87a7th9pd1.fsf@nightsong.com>
	<bbda04b9-0f91-47c5-9193-279b667f503c@googlegroups.com>
	<87h8no1nli.fsf@nightsong.com> <pcg2cc$h52$1@franka.jacob-sparre.dk>
	<874ljo1hvy.fsf@nightsong.com> <pcg6u7$hjr$1@franka.jacob-sparre.dk>
	<87vac4z2lh.fsf@nightsong.com> <pcimtl$2o5$1@franka.jacob-sparre.dk>
	<87lgcszjdn.fsf@nightsong.com> <pcvua5$cje$1@franka.jacob-sparre.dk>
	<pd11pn$n72$1@dont-email.me> <87sh6z1kkg.fsf@nightsong.com>
	<b169fddab8os90eqcnhm6ln2f30belp0ib@4ax.com>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: reader02.eternal-september.org;
 posting-host="4ad62473ff9dd9ec67a499bd743818bb";
	logging-data="12298"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1/LykO69YwfqkrAE5ykPTg9UOOAG91UzA4="
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.3 (darwin)
Cancel-Lock: sha1:ByEEKwy7ULSdbCxuUMfuzlkIj8g=
	sha1:oYvhL1PHKf1SamG8QaRgQPlu3KQ=
Xref: reader02.eternal-september.org comp.lang.ada:52207
Date: 2018-05-10T20:36:04+01:00
List-Id: <comp.lang.ada>

Dennis Lee Bieber <wlfraed@ix.netcom.com> writes:

> I have a strong suspicion that pre/post-conditions would be considered
> dead code to be removed from avionics software

If you've proved that the conditions won't be violated, you needn't
generate code to check them - any more than you need to generate code
for language-defined checks.

Then you end up passing invalid data to your inertial reference system
... oops