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!.POSTED!not-for-mail
From: Paul Rubin <no.email@nospam.invalid>
Newsgroups: comp.lang.ada
Subject: Re: Implicit actions & program correctness
Date: Fri, 15 May 2020 12:01:47 -0700
Organization: A noiseless patient Spider
Message-ID: <87y2ptc99g.fsf@nightsong.com>
References: <d4cc5c66-b82a-4ef7-8e69-2fa9b7bd99a6@googlegroups.com>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: reader02.eternal-september.org;
 posting-host="99a1eba264d96e9cdcb8b1129b02754c";
	logging-data="518"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1+7+BtGpBFMeDsNoq7iUXUM"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.1 (gnu/linux)
Cancel-Lock: sha1:vwRwhe0e8XQo+6KJhzhV/1Q4U5c=
	sha1:MzrPm73e9zGH5bcKLbi/R6BE9Tg=
Xref: reader01.eternal-september.org comp.lang.ada:58696
Date: 2020-05-15T12:01:47-07:00
List-Id: <comp.lang.ada>

deadhacker <gstover@gmail.com> writes:
> I guess another way to look at what I'm wondering is: In books about
> software engineering with Ada, I see lots of talk about correctness
> especially by moving bug detection to the compile phase.  How often
> can that actually be done?

Quite a lot, especially if you use fancier static checking like SPARK.
Programming errors can be classified into obvious silly ones, and more
subtle ones.  Decent compile time checking can catch most of the silly
ones.  That helps reliability and decreases testing workload, even if
you still have to deal with the remaining errors the usual ways.