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!nntp-feed.chiark.greenend.org.uk!ewrotcd!reality.xs3.de!news.jacob-sparre.dk!franka.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail
From: "Randy Brukardt" <randy@rrsoftware.com>
Newsgroups: comp.lang.ada
Subject: Re: Ada 2012 Constraints (WRT an Ada IR)
Date: Mon, 12 Dec 2016 18:41:31 -0600
Organization: JSA Research & Innovation
Message-ID: <o2ng3r$6nq$1@franka.jacob-sparre.dk>
References: <o2f8f5$ia2$2@franka.jacob-sparre.dk>
 <eb0po8Fgob2U1@mid.individual.net>
NNTP-Posting-Host: rrsoftware.com
X-Trace: franka.jacob-sparre.dk 1481589691 6906 24.196.82.226 (13 Dec 2016
 00:41:31 GMT)
X-Complaints-To: news@jacob-sparre.dk
NNTP-Posting-Date: Tue, 13 Dec 2016 00:41:31 +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; Response
Xref: news.eternal-september.org comp.lang.ada:32769
Date: 2016-12-12T18:41:31-06:00
List-Id: <comp.lang.ada>

"Niklas Holsti" <niklas.holsti@tidorum.invalid> wrote in message 
news:eb0po8Fgob2U1@mid.individual.net...
> 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.