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.dca1.giganews.com!nntp.giganews.com!goblin2!goblin.stu.neva.ru!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: {Pre,Post}conditions and side effects Date: Mon, 11 May 2015 19:15:27 -0500 Organization: Jacob Sparre Andersen Research & Innovation Message-ID: References: <2430252d-52a1-4609-acef-684864e6ca0c@googlegroups.com> <0a718b39-ebd3-4ab5-912e-f1229679dacc@googlegroups.com> <9ee5e186-5aaa-4d07-9490-0f9fdbb5ca18@googlegroups.com> <87tww5296f.fsf@adaheads.sparre-andersen.dk> <871tj9dp5b.fsf@theworld.com> <121ytg16vbxsk$.18dxo1h7daxty.dlg@40tude.net> NNTP-Posting-Host: rrsoftware.com X-Trace: loke.gir.dk 1431389727 21018 24.196.82.226 (12 May 2015 00:15:27 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Tue, 12 May 2015 00:15:27 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-RFC2646: Format=Flowed; Response X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157 Xref: number.nntp.giganews.com comp.lang.ada:193127 Date: 2015-05-11T19:15:27-05:00 List-Id: "Niklas Holsti" wrote in message news:cr5jl8Fee0jU1@mid.individual.net... > On 15-05-09 02:16 , Randy Brukardt wrote: >> "Niklas Holsti" wrote in message >> news:cr1snsF60hoU1@mid.individual.net... >>> On 15-05-07 22:01 , Randy Brukardt wrote: ... >>> Those are practical problems, not problems of principle. If you would >>> take >>> the same attitude to mathematics, you would claim that there are no >>> correct theorems. So I disagree with you. >> >> All programming is practical. We do not care about theorems, only that >> the >> current program is correct in the current environment. > > You have lost me here: you want to make the compiler prove things, but you > do not care about theorems, and do not want to be infected with a "theory" > disease? Is Humpty Dumpty involved somehow, making words mean whatever he > wants them to mean? :-) I see no value to "theorems" or "theory" per se; the value is in the techniques, not in those end results. In any case, after years of arguing with Dmitry here, I've learned to take on his best approaches to winning an argument. ;-) ... >> (another good reason for putting it into the compiler, as skipping the >> step >> isn't possible, and thus problems like the Ariene 5 don't happen). > > It is true that an optimizing and run-time-check-removing compiler has to > make the same kind of analyses and have the same kind of understanding of > the program's semantics as a program-proving tool. But constructing a > proof from scratch is expensive, unpredictably expensive, and possibly > non-terminating, while compilation of source code into machine code should > take a time that is reasonable, and reasonably predictable. I don't see that either is a given. Janus/Ada would run approximately forever if we didn't artifically bound the optimization time, and it still can take a long time to produce code. If we ever built the link-time code generation version, that time would go up by a lot. As with everything, one can make bad code quickly, or take longer to make good code. Similarly, I don't see any reason that proper proofs should take forever, as it is approximately the same problem as optimization and code generation. At some point, you give up and decide that something is unprovable. No big deal. > Hitherto, compilers have been expected to remove run-time checks that the > compiler can prove to itself are redundant, but not to remove *all* > redundant run-time checks. If the latter is required, compilation time > becomes unlimited -- a practical problem, no? If you want truly good code, compilation time should be nearly unlimited. But I agree that there is a practical limit, but the same limit applies to a proof tool (if you can wait 12 hours for a proof tool, you can wait 12 hours for a compilation, too, especially if one can turn that mode off or down, just like optimizers). ... > Ada has always had such features -- principally types, subtypes, ranges -- > and Ada 2012 has added more -- pre/post-conds and invariants. However, I'm > not sure if the features are yet sufficient to let us require, in the Ada > standard, that an Ada compiler should be able to prove (rather, to check) > exception-freeness, or termination, just to give two examples. Certainly not yet. One needs exception contracts at a minimum, as otherwise one cannot tell between exceptions raised as part of the behavior of a subprogram and those which represent bugs. > I believe it is a good goal for evolving Ada, but of course not the only > goal. I doubt that there is an "only goal", because lots of people have input. I happen to think it is the only goal that ulitmately matters, as much of the other ideas don't really move the needle in any significant way. > By the way, if exception contracts are added to Ada, termination contracts > should be considered, too. We already have "blocking" contracts on the drawing board. I don't quite see the point of termination contracts, a non-terminating subprogram is wrong 99.9% of the time. Maybe a "non-termination" contract would make some sense? Randy.