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!feeder.eternal-september.org!aioe.org!.POSTED.fn3LatRFkm9/xzEj7F2/NQ.user.gioia.aioe.org!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: Intervention needed? Date: Thu, 28 Mar 2019 10:06:20 +0100 Organization: Aioe.org NNTP Server Message-ID: 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> NNTP-Posting-Host: fn3LatRFkm9/xzEj7F2/NQ.user.gioia.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit X-Complaints-To: abuse@aioe.org User-Agent: Mozilla/5.0 (Windows NT 10.0; WOW64; rv:60.0) Gecko/20100101 Thunderbird/60.6.1 X-Notice: Filtered by postfilter v. 0.9.2 Content-Language: en-US Xref: reader01.eternal-september.org comp.lang.ada:55987 Date: 2019-03-28T10:06:20+01:00 List-Id: On 2019-03-28 08:01, Maciej Sobczak wrote: > 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? This is not how reasoning work. It is how the physical model does. Physical models have stochastic nature. The probabilistic measure is additive. But human reasoning is nowhere stochastic. > 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. Nothing like that. You have states the physical system may go into with different probabilities. Some of these states are fail-states. It has nothing to do with proofs. If something is proven about a physical system, that would be a fact, not a statistical event. Fact /= event. BTW, a digital system has an advantage that you can (theoretically) ensure some states never entered. You cannot do that with a physical system, there is always a non-zero probability that it would do nobody knows what. > The ability to work with continuous measures is what is practiced in every other engineering discipline (including critical ones!), yet the formal-method priests like you prevent me from deploying my acceptably correct programs. I find it a *limitation* of your methods, not mine. This again has nothing to do with measures, but with the Newtonian mechanics with limited masses and accelerations. The solutions there are smooth. Small changes of inputs produce small changes of outputs, except for few cases of chaotic systems etc. These premises do not apply to digital systems. Programming languages like Ada are designed in a way to smooth the behavior a bit, in order to allow gradual design, but only a bit. > 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 tools that are demonstrably unfit for today's market needs? Thank you. Very bad. This is a part of the problem as well. You cannot have it this way because old rules do not apply. Attempts to use quality assurance methods known in engineering disciplines to software result in nonsensical standards and certification procedures which assure nothing but wasting human resources. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de