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,FREEMAIL_FROM autolearn=unavailable autolearn_force=no version=3.4.4 X-Received: by 2002:a24:9d4a:: with SMTP id f71mr1866864itd.33.1553756501117; Thu, 28 Mar 2019 00:01:41 -0700 (PDT) X-Received: by 2002:aca:5757:: with SMTP id l84mr22921250oib.155.1553756500889; Thu, 28 Mar 2019 00:01:40 -0700 (PDT) Path: eternal-september.org!reader01.eternal-september.org!feeder.eternal-september.org!news.mixmin.net!proxad.net!feeder1-2.proxad.net!209.85.166.215.MISMATCH!78no138844itl.0!news-out.google.com!l81ni139itl.0!nntp.google.com!136no138781itk.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Thu, 28 Mar 2019 00:01:40 -0700 (PDT) In-Reply-To: <87a7hgvxnx.fsf@nightsong.com> Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=165.225.84.79; posting-account=bMuEOQoAAACUUr_ghL3RBIi5neBZ5w_S NNTP-Posting-Host: 165.225.84.79 References: <6e1977a5-701e-4b4f-a937-a1b89d9127f0@googlegroups.com> <6f9ea847-2903-48c8-9afc-930201f2765a@googlegroups.com> <87a7hgvxnx.fsf@nightsong.com> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <4e240c66-dce8-417f-9147-a53973681e29@googlegroups.com> Subject: Re: Intervention needed? From: Maciej Sobczak Injection-Date: Thu, 28 Mar 2019 07:01:41 +0000 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Xref: reader01.eternal-september.org comp.lang.ada:55984 Date: 2019-03-28T00:01:40-07:00 List-Id: > > For some N% of Ada programs, will a computation of a proof be > > predictably finished in time? .. Static knowledge is a privilege not > > shared by many, or much, I suppose. >=20 > If you haven't got some reasoning in your head that the program is > pointer-correct, you shouldn't deploy it. This is an appealing perspective, but I agree that the privilege is not ava= ilable in all situations (SPARK allows unchecked portions of code for a rea= son). Which brings a potentially interesting question - what if the reasoning in = my head has a continuous measure of correctness? Like, say, I'm 95% confide= nt that the reasoning is correct? Should I deploy my system or not? The mec= hanical proof will fail 100% of the time, but that does not mean that the s= oftware is entirely useless for my user, who also has his own continuous me= asure of risk and level of failure acceptance. The ability to work with continuous measures is what is practiced in every = other engineering discipline (including critical ones!), yet the formal-met= hod priests like you prevent me from deploying my acceptably correct progra= ms. I find it a *limitation* of your methods, not mine. Could you please fix your methods so that I can deploy my almost-certainly-= correct system, like everybody else does, instead of forcing me to use tool= s that are demonstrably unfit for today's market needs? Thank you. (disclaimer: playing the devil's advocate for a reason) --=20 Maciej Sobczak * http://www.inspirel.com