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 X-Received: by 2002:a05:660c:885:: with SMTP id o5mr6508811itk.27.1554131638892; Mon, 01 Apr 2019 08:13:58 -0700 (PDT) X-Received: by 2002:a05:6830:1192:: with SMTP id u18mr42478138otq.295.1554131638675; Mon, 01 Apr 2019 08:13:58 -0700 (PDT) Path: eternal-september.org!reader01.eternal-september.org!feeder.eternal-september.org!weretis.net!feeder6.news.weretis.net!feeder.usenetexpress.com!feeder-in1.iad1.usenetexpress.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!78no9686itl.0!news-out.google.com!r82ni30ita.0!nntp.google.com!136no9684itk.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Mon, 1 Apr 2019 08:13:57 -0700 (PDT) In-Reply-To: Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=96.255.209.31; posting-account=zwxLlwoAAAChLBU7oraRzNDnqQYkYbpo NNTP-Posting-Host: 96.255.209.31 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> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: Subject: Re: Intervention needed? From: Optikos Injection-Date: Mon, 01 Apr 2019 15:13:58 +0000 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Xref: reader01.eternal-september.org comp.lang.ada:56025 Date: 2019-04-01T08:13:57-07:00 List-Id: On Friday, March 29, 2019 at 4:39:13 AM UTC-4, Dmitry A. Kazakov wrote: > On 2019-03-29 07:57, Maciej Sobczak wrote: >=20 > > But I have read about ideas that even formal reasoning could exist in f= orms that trade efficiency against correctness. Think of it as an analog of= , say, image processing algorithms, which also can trade speed against reso= lution. >=20 > Each such reasoning, e.g. fuzzy or probabilistic inference can be=20 > reduced to a crisp reasoning about imprecise statements. E.g. a proof=20 > that the probability of E is greater than X. >=20 > > So you could have your program and various (continuous?) ways of choosi= ng between fast and exact and maybe your particular program is so complex t= hat exact reasoning would take more than a lifetime, whereas a reasonably h= igh level of confidence (but <100%) could be achieved in a timeframe that i= s acceptable for you and your customer. >=20 > No, you cannot. You can prove weaker propositions but that is not same.= =20 > There is no continuum of proofs. There might be some of propositions=20 > depending on the nature of things they state, in some few cases... >=20 > > What would you do? > >=20 > > Today you just ditch formal methods whatsoever and go on with laborious= testing. As if that was any wiser. >=20 > Right, but it is not a question of half-proofs about the same thing.=20 > IMO, the solution is proofs about things that can be proved leaving=20 > intractable issues aside. >=20 > I always wished SPARK integrated into Ada allowing the programmer to=20 > choose what to prove at the programming unit level without limiting the= =20 > language. >=20 > This especially applies to pointers. Leave them alone! There is no need= =20 > in accessibility checks or any limitations and ownership schemes. Just=20 > give exception contracts and let me prove no Constraint_Error=20 > propagating. Job done. Dmitry, I agree with nearly everything in reply to Maciej Sobczak on this t= hread=E2=80=94perhaps everything, depending on your answer to the following= . One clarifying question that I have is: how would you =E2=80=9Cprove no= Constraint_Error propagating=E2=80=9D? At run-time or at compile-time or = at engineering-time using tools other than the compiler? If at compile-time or at engineering-time using tools other than the compil= er, then that is the solution that ATS2 and ATS3 are pursuing, where ATS's = type views are rough analogues of what you are calling exception contracts = here. Paul Rubin, again thank you for the ATS tip. It is almost precisely what = I have been looking for. I've been having a blast learning ATS2 (and tryin= g to discern what is emerging in the ATS3 under development). SML meh. Ha= skell: meh. OCaml: better but still meh. MetaCaml: fascinating but still = meh. Coq not tightly integrated into OCaml: meh. ATS2+ATS/LF now that is= more like what I had in mind: rather smooth integration of multi-paradigm = dynamic programming language with VDM-esque/Z-esque (zed) stepwise refineme= nt with theorem prover with pointer correctness via type views. > >> But human reasoning is nowhere stochastic. > >=20 > > Paul asked for machine verification, so the limitations of human reason= ing need not bother us. > >=20 > >> BTW, a digital system has an advantage that you can (theoretically) > >> ensure some states never entered. > >=20 > > 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 confiden= ce (and therefore so called "certification credit") might have a continuous= measure. >=20 > That measure is useless as it does not apply to the system in question.= =20 > This by the way is the MAJOR flaw of certification procedures. The=20 > measure (confidence factor) applies to the *certifier*. It tells how=20 > much you managed to hide system faults from him. Amen. Certification of the people obfuscating software flaws, not certific= ation of the software, is what most certifications arrive at in the end. B= less their heart, their goals were almost correct, but without the (semi-au= tomated!) formal mathematical proofs at the foundation of the process, qual= ity certification is a fool's errand of people looking good, instead of mak= ing the software actually defect free. > > Of course, we don't yet have the formal methods with such capability, b= ut maybe the methods we have now are not fit for what we are trying to do w= ith them anyway. >=20 > There is a mountain of papers regarding confidence factors and their=20 > application. The only problem in connection to software design is that=20 > they are a measure of confidence in what you think rather than in what=20 > actually is. >=20 > --=20 > Regards, > Dmitry A. Kazakov > http://www.dmitry-kazakov.de