Re: {Pre,Post}conditions and side effects

[Niklas Holsti <niklas.holsti@tidorum.invalid>]

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:
>>> <Stefan.Lucks@uni-weimar.de> wrote in message
>>> news:alpine.DEB.2.11.1505071909280.16448@debian...
>>> ...
>>>> One property of a proper precondition (or postcondition or ...) is that
>>>> disabling the check does not change the functional behaviour of correct
>>>> programs.
>>>
>>> Sure, but this is irrelevant. There are no "correct" programs (in all
>>> possible senses). How do you know that you have a correct program? If you
>>> use some prover program, it too may have bugs. Or there might be bad data
>>> (cosmic rays?)
>>
>> 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? :-)

> Everything has to be reproved when anything changes

Agreed.

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

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?

To make proof a routine part of compilation, it has IMO to be reduced to 
*proof checking*. Checking a proof is fast and terminating.

To integrate proof-checking with compilation, the programming language 
has to be able to express the proof (axioms, lemmas, individual proof 
steps) interwined with the expression of the computation that is to be 
proved. And this has to be so easy that it tempts the programmer to 
write the proof -- or at least enough of the proof to guide the compiler 
-- as a routine part of creating the program. (Echoes here of 
proof-carrying code, http://en.wikipedia.org/wiki/Proof-carrying_code.)

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.

I believe it is a good goal for evolving Ada, but of course not the only 
goal.

By the way, if exception contracts are added to Ada, termination 
contracts should be considered, too.

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .