Re: Intervention needed?

[Optikos <optikos@verizon.net>]

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:
> 
> > 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.

Dmitry, I agree with nearly everything in reply to Maciej Sobczak on this thread—perhaps everything, depending on your answer to the following.  One clarifying question that I have is:  how would you “prove no Constraint_Error propagating”?  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 compiler, 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 trying to discern what is emerging in the ATS3 under development).  SML meh.  Haskell: 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 refinement with theorem prover with pointer correctness via type views.

> >> 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.

Amen.  Certification of the people obfuscating software flaws, not certification of the software, is what most certifications arrive at in the end.  Bless their heart, their goals were almost correct, but without the (semi-automated!) formal mathematical proofs at the foundation of the process, quality certification is a fool's errand of people looking good, instead of making the software actually defect free.

> > 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