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,FREEMAIL_FROM
	autolearn=unavailable autolearn_force=no version=3.4.4
X-Received: by 10.176.16.94 with SMTP id g30mr38282571uab.21.1481596461099;
        Mon, 12 Dec 2016 18:34:21 -0800 (PST)
X-Received: by 10.157.11.120 with SMTP id p53mr6135898otd.19.1481596461061;
 Mon, 12 Dec 2016 18:34:21 -0800 (PST)
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!1.eu.feeder.erje.net!feeder.erje.net!2.us.feeder.erje.net!newspeer1.nac.net!border2.nntp.dca1.giganews.com!nntp.giganews.com!p16no5947600qta.1!news-out.google.com!j8ni41176qtc.0!nntp.google.com!n6no5951377qtd.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Mon, 12 Dec 2016 18:34:20 -0800 (PST)
In-Reply-To: <o2ng3r$6nq$1@franka.jacob-sparre.dk>
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=67.0.242.189;
 posting-account=lJ3JNwoAAAAQfH3VV9vttJLkThaxtTfC
NNTP-Posting-Host: 67.0.242.189
References: <o2f8f5$ia2$2@franka.jacob-sparre.dk>
 <eb0po8Fgob2U1@mid.individual.net>
 <o2ng3r$6nq$1@franka.jacob-sparre.dk>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <b48d98ab-2b9b-47cd-b33e-674e07074c86@googlegroups.com>
Subject: Re: Ada 2012 Constraints (WRT an Ada IR)
From: Shark8 <onewingedshark@gmail.com>
Injection-Date: Tue, 13 Dec 2016 02:34:21 +0000
Content-Type: text/plain; charset=UTF-8
Xref: news.eternal-september.org comp.lang.ada:32771
Date: 2016-12-12T18:34:20-08:00
List-Id: <comp.lang.ada>

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.
> 
>                                                   Randy.

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?

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?