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:1awbjaens2vca$.1asmpnthmmycl.dlg@40tude.net...
> On Tue, 16 Jul 2013 17:13:43 -0500, Randy Brukardt wrote:
>
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>> news:1rjye7dyn3vgk.66fbcca9y4zd.dlg@40tude.net...
>>> On Mon, 15 Jul 2013 19:13:24 -0500, Randy Brukardt wrote:
>
>>>> Ada compilers do it all the time. The issue is letting the programmer
>>>> have access to that information.
>>>
>>> This is upside down. The programmer should manifest his intention for a
>>> constraint to hold and the compiler should verify that. The manifest 
>>> must
>>> be syntactically visible. Conflation such declaration with dynamic
>>> constraints is a bad idea.
>>
>> Yes, that's precisely what I'm talking about - some sort of exception
>> contract. But those don't depend on the kind of constraint.
>
> But they do, exception contract is a static constraint.
>
> It is no matter what is constrained, but how. Dynamically (=>code) vs.
> statically (=>proof).

Ah, you've redefined Ada's terms again. "Static" is defined in RM 4.9, and 
that's how I'm using it. "Proof", which is not an Ada concept, is not 
relevant to it's description.

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

It would be nice to have a discussion where you didn't change the 
terminology from that accepted by Ada (this is, after all, an Ada group).

...
>> it's an integrated part of the development
>> process. (Your program cannot be run if it doesn't compile.) Extra tools
>> never will have that level force behind them, and people like me would 
>> never
>> run them.
>
> I always was for SPARK being integrated into Ada.

Nothing that has body dependencies can be integrated into Ada.

...
>> But that's OK, there is no point in proving everything about everything.
>> Moreover, if you made this an expression function (meaning that you are
>> merely giving a name to "sqrt (A*B)", you could plug it in without any
>> effect on your proof. Enjoy.
>
> But you could prove that with concrete ranges of A and B at the client
> side. Which is the whole point. You want to discard a whole class of
> proofs.

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. The contract represented by the interface can be the 
*only* thing that clients depend upon. If they depend on anything else, 
changes to the body will break otherwise correct calls, and that's 
unacceptable. This property if absolutely required to build large programs 
with large and distributed teams -- otherwise, "proof" remains solely the 
provence of small, toy-sized programs.

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

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

>> 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, lots of allocated 
objects. (A major cause of "allocator mania" is certain other languages is 
that they don't have sufficiently powerful ways to create stack objects.)

In any case, we're talking about Ada here, and the form of Ada's I/O is 
fixed. The question is what proof techniques we can bring to these existing 
libraries, not how they could be designed in some hypothetical and 
unimplementable language.

                                         Randy.