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=-0.3 required=5.0 tests=BAYES_00, REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: The future of Spark . Spark 2014 : a wreckage Date: Fri, 12 Jul 2013 10:02:28 +0200 Organization: cbb software GmbH Message-ID: <1lhsyg46iz9jj.8jrvydqxt8l6.dlg@40tude.net> References: <1vc73wjwkqmnl$.gx86xaqy60u4$.dlg@40tude.net> <6pqhcwi0wuop.15v6h3g7gkto4.dlg@40tude.net> <1s6sw93u97355$.1n0205ucj6251.dlg@40tude.net> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: IenaDxMXK2hi7fvYcb+MlQ.user.speranza.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit X-Complaints-To: abuse@aioe.org User-Agent: 40tude_Dialog/2.0.15.1 X-Notice: Filtered by postfilter v. 0.8.2 Xref: news.eternal-september.org comp.lang.ada:16317 Date: 2013-07-12T10:02:28+02:00 List-Id: On Thu, 11 Jul 2013 17:28:31 -0500, Randy Brukardt wrote: > "Dmitry A. Kazakov" wrote in message > news:1s6sw93u97355$.1n0205ucj6251.dlg@40tude.net... >> 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). Firstly, you propose to replace proofs with tests, which automatically disqualifies the answer. Secondly, it does not work anyway. One famous example was given by Forsythe in his book on numerical methods. It is solving quadratic equation using school formula. In some cases (when roots are close to each other) the accuracy catastrophically drops for one root and increases for another. You *cannot* catch such stuff through tests. Only analysis can, and analysis is equivalent to proofs. >>>>> 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 *always* can do on the client's side: exception when Constraint_Error => Put_Line ("Oops!'); end; Which is the point, things are much simpler on instances of use compared to universal usage. >> 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. Really? You can start writing preconditions for +,-,*,/,** defined in the package Standard and continue to user defined types and subtypes. If anything is totally impractical then the idea to move Constraint_Error from post to pre-condition. It is wrong and will never work for anything beyond trivial examples. > If for whatever reason you can't do this, then yes you lose proveability. Nope. See above. I can prove that Constraint_Error is handled by given client. Which is what Ada programmers really want, because unhandled Constraint_Error is by far the most common bug. >> 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]). Most real cases are about downward closures and stuff when pointer is aliased argument. For the latter you need the body. >>> 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). This has nothing with that. Status_Error and Mode_Error are there because file type as designed does not reflect its mode: type Read_File_Type is ... type Write_File_Type is ... type Readwrite_File_Type is Read_File_Type and Write_File_Type is ... Done. > 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). This is a conflation of its worst. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de