Re: {Pre,Post}conditions and side effects

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

"Niklas Holsti" <niklas.holsti@tidorum.invalid> wrote in message 
news:cr5jl8Fee0jU1@mid.individual.net...
> On 15-05-09 02:16 , Randy Brukardt wrote:
>> "Niklas Holsti" <niklas.holsti@tidorum.invalid> 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.