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 From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: The future of Spark . Spark 2014 : a wreckage Date: Fri, 12 Jul 2013 16:16:36 -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> <1lhsyg46iz9jj.8jrvydqxt8l6.dlg@40tude.net> NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: loke.gir.dk 1373663797 23115 69.95.181.76 (12 Jul 2013 21:16:37 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Fri, 12 Jul 2013 21:16:37 +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 Path: border1.nntp.ams3.giganews.com!border1.nntp.ams2.giganews.com!border3.nntp.ams.giganews.com!border1.nntp.ams.giganews.com!nntp.giganews.com!eweka.nl!hq-usenetpeers.eweka.nl!212.27.60.7.MISMATCH!feeder1-1.proxad.net!proxad.net!feeder1-2.proxad.net!feed.ac-versailles.fr!news.ecp.fr!news.jacob-sparre.dk!loke.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail X-Original-Bytes: 8088 Xref: number.nntp.dca.giganews.com comp.lang.ada:182503 Date: 2013-07-12T16:16:36-05:00 List-Id: "Dmitry A. Kazakov" wrote in message news:1lhsyg46iz9jj.8jrvydqxt8l6.dlg@40tude.net... > 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. True enough. I'm saying that we need to replace the impractical ("proofs") with the possible. > 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. If your "cookbook" is full of bad algorithms, then of course you'll get garbage. And I certainly agree you can't test accuracy. The problem is that even if you prove that your algorithm is too inaccurate, what can you do? You don't have any other way to implement it (because you already did the research to find the best algorithm available -- if you didn't do at least that, "proof" is the LEAST of your problems). I was presuming that you were starting with a cookbook implementation of appropriate accuracy, and the only need for testing is to prove that the algorithm was in fact implemented properly. If you're starting with a blank sheet of paper, there is no technique that is likely to be available in my lifetime that is reaally going to help. ... >>> 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; That doesn't prove that the constraint is not violated -- that's proving that you covered it up! Supposedly, it's the worst side-effect of exception contracts in Java, is that programmers write handlers to swallow exceptions without knowing or caring why they're doing so. You've got to prevent the exceptions at the source, and the main way you do that for Constraint_Error is to use proper range constraints and null exclusions on parameters. Then your proof is actually possible because we moved it from inside of the body to the call site. > Which is the point, things are much simpler on instances of use compared > to > universal usage. Which of course is what I've been saying: you move these requirements into the contract for a subprogram so you can prove them at the call-site. It's impossible to prove anything in the body of a subprogram if all of the parameters are type Integer. >>> 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. Which is amazing because it works for most examples. (It doesn't work for overflow of "*" very well, but that's the only real issue.) And in any case, there is no point in moving it for language-defined operators -- both the compiler and any provers know exactly what they do. It's only for user-defined subprograms that you need to do so. ... >>>> 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. Huh? This makes no sense for this problem. You can't do that in any version of Ada (or any other sensible language), because it would require that the type of a file object could change in response to operations. And in such a language, it would be impossible to do any static checks (you can't know if Open is going to succeed, for instance, so afterwards, the file is going to have one of several possible types). Which would defeat the purpose. Ada doesn't allow changing the type of an object for any reason, and to change that would require designing a new language. I realize that you have a fantasy that such a radical redesign could be made to work compatibly, but that's highly unlikely. >> 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. Carried over from Ada 83. Ada will never be a language that requires much in the way of proof, it would be way too disruptive to existing implementations. (And we definitely want more than one implementation!). It could only be changed in a new Ada-like language, but that seems unlikely right now. Randy.