Re: {Pre,Post}conditions and side effects

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

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:1ftovlipftuej.p27p4vog2ka6.dlg@40tude.net...
> On Thu, 07 May 2015 11:01:26 +0200, Georg Bauhaus wrote:
>> On 06.05.15 23:07, Randy Brukardt wrote:
>>> In order for proof to
>>> be part of the compiler, the proof language has to be part of the 
>>> language.
>>
>> If the proof language is understood by the compiler, this does not
>> require it to be compilable Ada, or efficiently computable (and
>> terminating in time), I think?
>
> A compiler compiles, evidently...
>
> The fallacy of Randy's conclusion is different. A compiler need not to be
> the compiler from single language.

True enough. I was going to refute that in my original message, but I 
thought it would be rambling.

I personally am from the camp that thinks that Ada is the best possible 
language for commicating anything. (Well, other than with other humans, but 
that's the fault of the humans and not the language. ;-) [That's certainly 
true of the expression syntax, there might be some room for improvement in 
declarations.] If something can't be expressed in Ada, it's not worth 
expressing (I see no value to incomputable things).

> 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. After all, developing in Ada 
already has a reputation for being slow, doubling that time is never going 
anywhere outside of narrow niches. 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.) That makes proof 
most valuable when applied to runtime checks, such as Ada 2012 assertions, 
or simply explicit code of a similar form.

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. You end up writing the program twice in two different languages. 
That might have value in extreme circumstances (loss of life potential), but 
most programs are not like that (my spam filter, for example, or our Ada 
compiler).

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

                                     Randy.