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 Newsgroups: comp.lang.ada Subject: Re: Intervention needed? Date: Thu, 28 Mar 2019 00:17:35 -0700 Organization: A noiseless patient Spider Message-ID: <877ecjwjqo.fsf@nightsong.com> References: <6e1977a5-701e-4b4f-a937-a1b89d9127f0@googlegroups.com> <6f9ea847-2903-48c8-9afc-930201f2765a@googlegroups.com> <87a7hgvxnx.fsf@nightsong.com> <4e240c66-dce8-417f-9147-a53973681e29@googlegroups.com> Mime-Version: 1.0 Content-Type: text/plain Injection-Info: reader02.eternal-september.org; posting-host="d5e4160589035e62287c9c28a478db11"; logging-data="17370"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX18rj8M1P6Ppy2mIARuMeHUb" User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.3 (gnu/linux) Cancel-Lock: sha1:zpVnAygscVnWRm0+mJ/G5rT9JQc= sha1:0pSH6EYZIE5IW3O1PrW8CQ3YYOY= Xref: reader01.eternal-september.org comp.lang.ada:55985 Date: 2019-03-28T00:17:35-07:00 List-Id: Maciej Sobczak 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.