Re: The future of Spark . Spark 2014 : a wreckage

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

On Tue, 9 Jul 2013 15:37:10 -0500, Randy Brukardt wrote:

>> There are obviously goals which cannot be proven without the bodies. Proofs
>> about specifications are important but far not all. Consider LSP as an
>> example. You cannot prove substitutability from interfaces. It simply does
>> not work. Same with almost everything else, because proving something in
>> general is much more harder, even impossible, than proving things about a
>> concrete instance, e.g. body.
> 
> My contention is such things are not worth proving. With strong enough 
> contracts (including class-wide contracts for dispatching calls, and 
> contracts on subprogram types :-), important properties of code can be 
> proven.

No, that is the problem. You want to overburden the contracts with stuff
that does not belong there. This would make the design fragile.

Consider as an example stack use. Do you want to contract all subprograms
to maximum stack use, or let the compiler to estimate stack use of a
concrete body?

Another example is a mathematical function like sine. In order to prove its
correctness you would need an extremely elaborated apparatus of contract
specification which itself will be a source of countless bugs due to its
complexity. This is a typical over-specification. Only if somebody wanted
to verify an implementation of sine, he would have to look into the body.
Most people never will.

Contracts should not define semantics, only most general properties of. Yet
semantics should sometimes be proven. The provider does not know when. It
is up to the user. In that case he have to look into the body.

> What's too hard shouldn't be bothered with, because we've lived just 
> fine with no proofs at all for programming up to this point.

We didn't. Accessibility checks and constraint errors are a permanent
headache in Ada.

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