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:1vc73wjwkqmnl$.gx86xaqy60u4$.dlg@40tude.net...
> On Mon, 8 Jul 2013 16:32:21 -0500, Randy Brukardt wrote:
>
>>> I realy hope that Spark users will say to AdaCore that they aro going
>>> wrong and that AdaCore will really try to make a better future for 
>>> Spark.
>>
>> Spark users are on a certain dead-end, IMHO. The future is getting proof
>> into the hands of all programmers, as a normal part of their day-to-day
>> programming. That requires that proofs aren't necessarily complete,
>
> Rather the programmer should announce what to prove and that proof must be
> complete.

Right. And that should be an integral part of compilation: no proof, no 
compilation.

>> that
>> they use whatever information is available, and most of all, that they 
>> only
>> depend on the specifications of packages (never, ever, on the contents of 
>> a
>> body).
>
> 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. 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. Proofs should 
be an aid to debugging, not the be-all, end-all. I want to add proof 
technology incrementally so that everyone can use a little of it, benefit 
from it, and then use more of it. It's how most Ada programmers learned to 
use types and constraints, and its the way to get proofs into the 
mainstream. Not by stand-alone tools and subsets with weird rules.

                                   Randy.


                                            Randy.