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

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

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:6pqhcwi0wuop.15v6h3g7gkto4.dlg@40tude.net...
> 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?

As I said, these sorts of things aren't worth proving. Certainly not until 
proof of simple concepts is already a widely used feature of Ada; then 
expanding it further might make sense. But we have to walk before we can 
run, and we're barely crawling right now.

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

There is no reason to prove such things. For things like Sine, the best one 
can do is copy an implementation from a cookbook -- it makes no sense to 
even imagine trying to create a new one. (That makes as much sense as 
creating a new sort.) Even the simplest tests will detect any implementation 
errors (and we're never going to be able to live without testing).

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

Constraint_Errors a headache? They're a blessing, because the alternative is 
zillions of impossible to find bugs. (I lived with those in the early days 
of Janus/Ada; I'll never go back.) It will never, ever be possible to detect 
every runtime failure at compile-time, nor is it possible to pre-test 
because of the possiblity of race conditions, so we have to have 
Constraint_Error.

It's annoying that one can't tell between specification errors that should 
be contracted and proved away and those that are truly runtime (that is, a 
normal part of the implementation); Ada does conflate these things and 
that's probably annoying to a purist. (You can't seem to see the difference, 
which leads to bizarre conclusions.) But it's far from fatal.

                                          Randy.