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: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!gandalf.srv.welterde.de!news.jacob-sparre.dk!franka.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: Ada 2012 Constraints (WRT an Ada IR) Date: Tue, 13 Dec 2016 16:35:25 -0600 Organization: JSA Research & Innovation Message-ID: References: NNTP-Posting-Host: rrsoftware.com X-Trace: franka.jacob-sparre.dk 1481668525 3749 24.196.82.226 (13 Dec 2016 22:35:25 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Tue, 13 Dec 2016 22:35:25 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157 X-RFC2646: Format=Flowed; Original Xref: news.eternal-september.org comp.lang.ada:32794 Date: 2016-12-13T16:35:25-06:00 List-Id: "Shark8" wrote in message news:b48d98ab-2b9b-47cd-b33e-674e07074c86@googlegroups.com... > On Monday, December 12, 2016 at 5:41:32 PM UTC-7, Randy Brukardt wrote: >> "Niklas Holsti" wrote: >> >> > On 16-12-09 23:41 , Randy Brukardt wrote: >> ... >> >> Trying to put a predicate logic prover into a compiler optimizer >> >> sounds >> >> challenging at best. >> > >> > I'm a little surprised: I seem to remember that you have, earlier, said >> > that you would like future compilers to prove all sorts of things about >> > the program. But you were not thinking of predicate logic proofs? >> >> Potentially different parts of the compiler. And, no, I wasn't thinking >> of >> predicate logic proofs so much as simple common subexpression >> elimination, >> algebraic reductions, flow analysis, and other existing, common >> optimization >> techniques. The problem with these is more in usefully reporting the >> results >> to the user than with actually doing them (as they likely already exist >> in >> compilers, but tend to be used on lower-level code formats). In >> particular, >> one would want to report to the user when a precondition or postcondition >> cannot be optimized to "True", but how to do that usefully (in the >> back-end >> of a compiler where little source information remains), and especially >> avoiding too much nattering, isn't obvious to me. >> > > I think I see. You're talking something more like this -- > http://citeseer.ist.psu.edu/viewdoc/download;jsessionid=46530BCDD09D9D8B41C7FE958AAD0442?doi=10.1.1.53.1099&rep=rep1&type=pdf - > - no? When I tried to open that link, my browser crashed, so I didn't look at it. But probably. My primary goal here has always been to optimize Pre/Post/predicates well enough that it isn't necessary to ignore them. Since these are just more powerful constraints, and constraint checks shouldn't be suppressed unless all else fails, it seems to me that the same dynamic should apply to contract assertions. And practically, that has to be done mainly with the existing engines in an Ada compiler; adding a lot more complexity to one is likely to result in an unmaintainable mess. (They're already close to the boundary of what's practical, IMHO.) > But constraint-engines are certainly needed for (e.g.) SPARK for its SMT > (satisfiability modulo theory) > solver/prover... would it be a bad idea to further integrate these into > the [non-restricted Ada] compiler? Surely not a bad idea, but I think it's likely to be impractical. I suppose if someone started from scratch with proof in mind, they could replace a lot of optimization code with proof -- but is anyone really going to start a project like that from scratch these days? (Having a proof engine is not going to make Ada visibility and resolution any easier to implement.) Randy.