Re: {Pre,Post}conditions and side effects

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Thu, 7 May 2015 13:32:28 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:1ftovlipftuej.p27p4vog2ka6.dlg@40tude.net...

>> The proof language is another language. It cannot be same language because 
>> that is inconsistent.
> 
> I completely disagree here. If one is required to write separate proof 
> instructions, hardly anyone would do it.

Still it cannot be the same language. But many, including me, would gladly
add proof instructions to critical parts of the program. And this should
not preclude sharing same source files for both languages.

> After all, developing in Ada 
> already has a reputation for being slow, doubling that time is never going 
> anywhere outside of narrow niches.

It would meet much more acceptance if adding proof would not be obligatory.
I see it as a great advantage too. "Write first, prove later" might sound
not much like Ada attitude, but I am sure most programmers will gladly
embrace this approach. Most programmers do code cleanup, review,
beautification anyway. Adding proofs naturally fits into this phase.

> The value of proof, IMHO, is in finding 
> runtime failures at compile time, both because that will generate better 
> code, and because earlier detection of errors is better. (This becomes even 
> more useful in the face of exception contracts, because absence of an 
> exception is then either proved or the program is illegal.)

Yes.

> I don't find any value in proving the "correctness" of code (whatever that 
> means), because the description of what the code does is going to be at 
> least as complex as the code itself, and thus at least as susptible to 
> errors.

It adds another layer of safety. It also gives another perspective on the
program's overall design. Proofs consider the program as a whole with all
possible states of, while run time checks and tests deal with only a very
small subset of states.

> You end up writing the program twice in two different languages.

That is the idea. But it is not *the* program. The program is written only
once in Ada. The proofs are written *for* this program, they do not change
the program itself. Though proofs may hint the programmer to redesign
certain parts of the program.

> So one language for the majority of us doing "normal" things; perhaps two 
> languages for extreme cases (but I'm not remotely interested in that - 
> thinks like SPARK are terribly limiting).

That is because of all or nothing attitude. Proofs must be really optional.
They should not be required in upfront design.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de