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: Fri, 29 Mar 2019 09:39:11 +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> <28b6a472-6c3a-40a6-8a96-2e27a65ab2ef@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 Content-Language: en-US X-Notice: Filtered by postfilter v. 0.9.2 Xref: reader01.eternal-september.org comp.lang.ada:55993 Date: 2019-03-29T09:39:11+01:00 List-Id: On 2019-03-29 07:57, Maciej Sobczak wrote: > But I have read about ideas that even formal reasoning could exist in forms that trade efficiency against correctness. Think of it as an analog of, say, image processing algorithms, which also can trade speed against resolution. Each such reasoning, e.g. fuzzy or probabilistic inference can be reduced to a crisp reasoning about imprecise statements. E.g. a proof that the probability of E is greater than X. > So you could have your program and various (continuous?) ways of choosing between fast and exact and maybe your particular program is so complex that exact reasoning would take more than a lifetime, whereas a reasonably high level of confidence (but <100%) could be achieved in a timeframe that is acceptable for you and your customer. No, you cannot. You can prove weaker propositions but that is not same. There is no continuum of proofs. There might be some of propositions depending on the nature of things they state, in some few cases... > What would you do? > > Today you just ditch formal methods whatsoever and go on with laborious testing. As if that was any wiser. Right, but it is not a question of half-proofs about the same thing. IMO, the solution is proofs about things that can be proved leaving intractable issues aside. I always wished SPARK integrated into Ada allowing the programmer to choose what to prove at the programming unit level without limiting the language. This especially applies to pointers. Leave them alone! There is no need in accessibility checks or any limitations and ownership schemes. Just give exception contracts and let me prove no Constraint_Error propagating. Job done. >> But human reasoning is nowhere stochastic. > > Paul asked for machine verification, so the limitations of human reasoning need not bother us. > >> BTW, a digital system has an advantage that you can (theoretically) >> ensure some states never entered. > > But I'm not talking about system states, but about our confidence that a given state will be achieved or not. States can be discrete, but confidence (and therefore so called "certification credit") might have a continuous measure. That measure is useless as it does not apply to the system in question. This by the way is the MAJOR flaw of certification procedures. The measure (confidence factor) applies to the *certifier*. It tells how much you managed to hide system faults from him. > Of course, we don't yet have the formal methods with such capability, but maybe the methods we have now are not fit for what we are trying to do with them anyway. There is a mountain of papers regarding confidence factors and their application. The only problem in connection to software design is that they are a measure of confidence in what you think rather than in what actually is. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de