Path: ...!3.eu.feeder.erje.net!feeder.erje.net!fu-berlin.de!uni-berlin.de!individual.net!not-for-mail
From: Bill Findlay <findlaybill@blueyonder.co.uk>
Newsgroups: comp.arch
Subject: Re: Computer architects leaving Intel...
Date: Mon, 16 Sep 2024 22:40:33 +0200
Organization: none
Lines: 23
Message-ID: <0001HW.2C98CF41017414F8306B4D38F@news.individual.net>
References: <2024Aug30.161204@mips.complang.tuwien.ac.at> <vbcob9$dvp4$1@dont-email.me> <vbd6ia$e0ld$2@dont-email.me> <UxpCO.174965$Hld5.7714@fx15.iad> <vc41rl$1fhjd$1@dont-email.me> <2024Sep14.152652@mips.complang.tuwien.ac.at> <d93c1dc0455692767c89ea9f7bd47ed1@www.novabbs.org> <vc4o0l$1kuqf$1@dont-email.me> <vc6vno$285g2$1@dont-email.me> <vc8qor$2od9v$1@dont-email.me> <vc99fi$2re3k$2@dont-email.me> <20240916160402.0000087f@yahoo.com> <vc9e72$2smso$1@dont-email.me> <tkYFO.77534$kxD8.10093@fx11.iad> <20240916185857.000011ef@yahoo.com> <lkradoFp9aeU1@mid.individual.net>
Reply-To: findlaybill@blueyonder.co.uk
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Transfer-Encoding: 7bit
X-Trace: individual.net Kzb2ePV/fZ1FjmbhFj+ejQLdJdAX753TvJ/qnKuWLoMfCFtLYT
X-Orig-Path: not-for-mail
Cancel-Lock: sha1:d7LzciAEDArrDt7FqFjieKeJmSY= sha256:qZFpFho5bC+43Fg9wob02/R37vV8Lbp29xwDr5dt0cI=
User-Agent: Hogwasher/5.24
Bytes: 2243

On 16 Sep 2024, Niklas Holsti wrote
(in article <lkradoFp9aeU1@mid.individual.net>):
....
> The recommended approach today (for applications where it matters) is to
> use static analysis of the Ada code (e.g. SPARK or other tools) to prove
> that run-time errors cannot happen, which then makes it possible to omit
> the corresponding run-time checks while staying compliant.
>
> I don't know if Rust code can be analysed as easily and completely as
> Ada code can. But Ada compilers usually allow fine-grained control over
> which checks are applied where, not just a single choice between "debug"
> and "production" builds.

I find, without using SPARK or any analysis (other than that done
by the compiler) that going from all Ada language-defined checks
ON to all OFF gains <  5% in speed.

So all checks are left ON in "production" builds.

-- 
Bill Findlay