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

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

On Wed, 17 Jul 2013 18:26:31 -0500, Randy Brukardt wrote:

> By your twisted definition, everything is static (including dynamic 
> constraints!) if sufficient information is known at compile-time to reason 
> about them.

Yes.
 
> Absolutely. The sorts of proofs you want would absolutely kill program 
> maintenance, making it impossible to have the sort of reusable libraries 
> that Ada makes so easy.

Maybe. But remember that other proofs will be useless beyond toy cases.

>> Especially the ones crucial for exception contracts. How are you
>> going to prove the caller's contract not to raise? You could not without
>> non-sensual handlers. It would be like the idiotic "function must have a
>> return statement rule."
> 
> You can only provide exception contracts if you have strong preconditions 
> and constraints on the parameters. In the absense of that, you shouldn't be 
> *allowed* to prove anything, because in doing so you force a strong coupling 
> to the contents of the body.

As I said. Useless. 

>>>> Opening readonly file for writing is not a bug it is an error, a  legitime
>>>> state of the program which must be handled. Writing a file opened as
>>>> readonly is a bug. Bug /= error. Errors are handled, bugs are fixed.
>>>
>>> You claim that you can use the file type to eliminate Status_Error and
>>> Mode_Error. But that's impossible, because an Open that fails leaves the
>>> file unopened;
>>
>> This is another issue, i.e. construction and initialization. You should 
>> not be able to create unopened instances of file type.
> 
> Nice theory, impossible to do in practice.

Even if as "practice" you mean broken limited return, it is still quite
possible.

>>> and you have to be able to fall back and open a different
>>> file (or create one instead) on such a condition. It's not practical to 
>>> have a single Open operation as an initializer
>>
>> Why? I certainly want it exactly this way.
> 
> It's impractical to have an Open that somehow encodes every possible 
> sequence of Open-fall back-Open-Create that might come up. In the absense of 
> that, you have to resort to complex program structures (it's not possible to 
> declare objects with the right scope easily) or worse,

It won't be any more complex than it is when handling exceptions
propagating out of Open. In fact it will be much simpler because you forgot
the issue of closing the file on subsequent errors.

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