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: border1.nntp.dca3.giganews.com!border2.nntp.dca3.giganews.com!border4.nntp.dca.giganews.com!border2.nntp.dca.giganews.com!nntp.giganews.com!usenet.blueworldhosting.com!feeder02.blueworldhosting.com!reality.xs3.de!news.jacob-sparre.dk!loke.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: The future of Spark . Spark 2014 : a wreckage Date: Thu, 11 Jul 2013 17:28:31 -0500 Organization: Jacob Sparre Andersen Research & Innovation Message-ID: References: <1vc73wjwkqmnl$.gx86xaqy60u4$.dlg@40tude.net> <6pqhcwi0wuop.15v6h3g7gkto4.dlg@40tude.net> <1s6sw93u97355$.1n0205ucj6251.dlg@40tude.net> NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: loke.gir.dk 1373581713 20134 69.95.181.76 (11 Jul 2013 22:28:33 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Thu, 11 Jul 2013 22:28:33 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-RFC2646: Format=Flowed; Original X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157 X-Original-Bytes: 6032 Xref: number.nntp.dca.giganews.com comp.lang.ada:182473 Date: 2013-07-11T17:28:31-05:00 List-Id: "Dmitry A. Kazakov" wrote in message news:1s6sw93u97355$.1n0205ucj6251.dlg@40tude.net... > On Wed, 10 Jul 2013 18:21:33 -0500, Randy Brukardt wrote: > >> "Dmitry A. Kazakov" wrote in message >> news:6pqhcwi0wuop.15v6h3g7gkto4.dlg@40tude.net... > >>> Another example is a mathematical function like sine. In order to prove >>> its >>> correctness you would need an extremely elaborated apparatus of contract >>> specification which itself will be a source of countless bugs due to its >>> complexity. This is a typical over-specification. Only if somebody >>> wanted >>> to verify an implementation of sine, he would have to look into the >>> body. >>> Most people never will. >> >> There is no reason to prove such things. For things like Sine, the best >> one >> can do is copy an implementation from a cookbook -- it makes no sense to >> even imagine trying to create a new one. > > Do you have Hankel function in your cookbook? Don't know what it is, so I'd never try to write one. > How do you know that the copy you made is authentic? What is about the > accuracy of the implementation? That's easily determinable by unit tests (which are needed in any case - testing and proof are not exclusive, you need both because it's real easy to prove the wrong thing). If you screw up copying a cookbook function, you'll get results that are obviously wrong, and that's easy to detect. >>>> What's too hard shouldn't be bothered with, because we've lived just >>>> fine with no proofs at all for programming up to this point. >>> >>> We didn't. Accessibility checks and constraint errors are a permanent >>> headache in Ada. >> >> Constraint_Errors a headache? They're a blessing, because the alternative >> is >> zillions of impossible to find bugs. > > No, the alternative is to prove that the constraint is not violated. That's completely impractical. > You can do this only at the client side. Which is why it cannot be > contracted for the callee. When you move from instances to universally > holding contracts you frequently lose provability. ...of things that aren't worth proving in the first place. You get rid of constraint_errors from bodies by writing good preconditions, predicates, constraints, and exclusions in the first place. Have constraint_error from dereferencing a null pointer? Use an exclusion (or a pre-test). Same with ranges or with user properties. If for whatever reason you can't do this, then yes you lose proveability. But that's the price of lowering coupling, and excessive coupling is the cause of almost all software inflexibility. > Note how accessibility checks attempted in the form of a contract became > more problem than solution. In order to have it provable you must > strengthen it. Probably every Ada programmer was annoyed by silly "must be > statically deeper" messages about pointers. It cannot be handled at the > level of contracts. Yet in most cases it is no problem to see that a > *given* pointer is never dangling. "No problem"? Informally, sure. It's impossible to prove in any real case; there is too much going on. (Claw, for instance, prevents it by design, but I don't think there is any way to formally describe that design -- certainly not in systems like Spark which ignore the effects of finalization [which is how Claw guarentees non-dangling]). >> It's annoying that one can't tell between specification errors that >> should >> be contracted and proved away and those that are truly runtime (that is, >> a >> normal part of the implementation); > > That was ARG's decision for Ada 2012, wasn't it? No, it was an effect of Ada 83, which conflated those uses of exceptions. We had to formalize existing practice (we need the ability to add these specifications to existing code without changing any behavior). It would be better for exceptions that we would want to "prove-away" (like Status_Error and Mode_Error in Text_IO) to be strictly separated from those that are purely runtime behavior (like End_Error and Device_Error). One thing we had to do is to make these things work is to allow existing compilers to use runtime checks, with the hope that more will become proved over time. Compiler technology isn't quite ready for mandatory proof requirements (maybe next time). >> Ada does conflate these things and >> that's probably annoying to a purist. (You can't seem to see the >> difference, >> which leads to bizarre conclusions.) But it's far from fatal. > > It is fatal, because inconsistent. Error /= bug. We can only agree to disagree on that. Randy.