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

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

On Tue, 09 Jul 2013 12:29:03 +0100, Simon Wright wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> 
>> On Mon, 8 Jul 2013 16:32:21 -0500, Randy Brukardt wrote:
> 
>>> 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.
> 
> I think what Randy meant (and may even have said) was that in
> 
>    with A;
>    package B is ...
> 
> it shouldn't be necessary to look at the body of A to prove the body of
> B. Of course the body of A will have to be proved ... but not right now.

Yes this is how I understood him and what I objected to.

You cannot rely on the contracts when it comes to correctness.

OK, for the sake on the argument, you could contract proofs about A's body,
so that these proofs could be used in the proofs of the body B. But the
problem with that is exactly what Randy wanted to avoid - tight coupling
and doing things in advance which nobody would ever needed.

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