Re: Ada 2012 Constraints (WRT an Ada IR)

["Randy Brukardt" <randy@rrsoftware.com>]

"Shark8" <onewingedshark@gmail.com> 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.