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: Intervention needed?
Date: Fri, 29 Mar 2019 00:13:35 -0700
Organization: A noiseless patient Spider
Message-ID: <87bm1uxie8.fsf@nightsong.com>
References: <b196da6e-4614-42f9-9147-b1708c6e5094@googlegroups.com>
	<a534f338-a418-424e-8043-31c738682807@googlegroups.com>
	<q68mv0$rea$1@dont-email.me>
	<a4ab4f3c-9151-47c7-9d3f-f6a23451fa0e@googlegroups.com>
	<bba8f6a8-36ce-4bed-bd84-8a9ea7dc02f7@googlegroups.com>
	<q699nu$ban$1@franka.jacob-sparre.dk>
	<6e1977a5-701e-4b4f-a937-a1b89d9127f0@googlegroups.com>
	<q6pa1g$3j7$1@franka.jacob-sparre.dk>
	<6f9ea847-2903-48c8-9afc-930201f2765a@googlegroups.com>
	<q6qa4u$kd0$1@gioia.aioe.org>
	<f4eee526-e607-4e1f-843f-9913c9c093f9@googlegroups.com>
	<q6rphu$arn$1@franka.jacob-sparre.dk>
	<f610da94-1309-4cb6-8c7b-47f3099381e5@googlegroups.com>
	<q71hbi$aua$1@franka.jacob-sparre.dk> <q728mu$5je$1@gioia.aioe.org>
	<b4dd0ab5-7698-4a03-b119-a4ce0be208a8@googlegroups.com>
	<q7giel$bdv$1@dont-email.me> <87a7hgvxnx.fsf@nightsong.com>
	<4e240c66-dce8-417f-9147-a53973681e29@googlegroups.com>
	<q7i2qb$bqn$1@gioia.aioe.org>
	<28b6a472-6c3a-40a6-8a96-2e27a65ab2ef@googlegroups.com>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: reader02.eternal-september.org;
 posting-host="b6ad68bdf16a0e4015fe5cb5464f5f2f";
	logging-data="32031"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1/E0v7rVBI9Rp+BVwjiSPK0"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.3 (gnu/linux)
Cancel-Lock: sha1:hqjVn8npTQDtAhNNv9zihgtzXb4=
	sha1:avaNTuO7r+bSfNZNVVx0t+12LCQ=
Xref: reader01.eternal-september.org comp.lang.ada:55991
Date: 2019-03-29T00:13:35-07:00
List-Id: <comp.lang.ada>

Maciej Sobczak <see.my.homepage@gmail.com> writes:
> Paul asked for machine verification, so the limitations of human
> reasoning need not bother us.

Systems like SPARK don't do any significant amount of automatic
reasoning.  You do the reasoning in your own head in the usual way.
SPARK them lets you write the reasoning down in a precise enough way
that the verifier can check it.  It's just like how the Ada compiler (or
some other programming language) lets you write down the computational
steps of your algorithm in a precise enough way that the machine can
execute it.

> a continuous measure. Of course, we don't yet have the formal methods
> with such capability, 

Sure we do.  For example, probabilistic algorithms are a thing.  Or you
could prove that with a given distribution of input values, your
algorithm will succeed 98.235% of the time.  There might be some kinds
of tasks for which that is sufficient, especially if you can detect the
failed instances and reprocess them.

Usually though, one resorts to formal methods in order to eliminate as
much uncertainty as possible.  So if you need a bounded WCET you won't
use a hash table, or that type of thing.