Re: Intervention needed?

[Paul Rubin <no.email@nospam.invalid>]

Maciej Sobczak <see.my.homepage@gmail.com> writes:
> Which brings a potentially interesting question - what if the
> reasoning in my head has a continuous measure of correctness? Like,
> say, I'm 95% confident that the reasoning is correct? Should I deploy
> my system or not? The mechanical proof will fail 100% of the time, but
> that does not mean that the software is entirely useless for my user,
> who also has his own continuous measure of risk and level of failure
> acceptance.

I would say that in a high-assurance system (which is the normal
situation where one talks about SPARK and proofs), what you describe is
by definition not allowed.  That's using the notion of high-assurance
software from here:

https://dwheeler.com/essays/high-assurance-floss.html

Of course you could redefine your system to be medium-assurance and let
it through.  Usually that type of software is validated through more
conventional testing processes.

Fwiw, there's a video on Youtube of Adacore founder Bob Dewar talking
about the flight software for the F-22 fighter plane, where he asks
whether that software should be considered safety-critical.  The
audience laughs, but Dewar goes on to say that of course a passenger
plane's software is safety-critical, but the whole idea of a fighter
plane is to go up and get shot at, the controls let the pilot
deliberately run the engines above their power envelope, etc.  IIRC he
said that the F-22 program managers didn't buy that argument and still
wanted the software to be treated as safety-critical.

Be careful too of "normalization of deviance", the sociological process
that led the Space Shuttle staff to accept more and more misbehaviour
from the Shuttle until the Challenger exploded.  The term is from Diane
Vaughan's book "The Challenger Launch Decision", which I want to get
around to reading someday.