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

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

On Mon, 15 Jul 2013 19:13:24 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:1d4tuwlfdnz2j$.18l68s96x3vjj.dlg@40tude.net...
>> On Fri, 12 Jul 2013 16:16:36 -0500, Randy Brukardt wrote:
> ...
>>> You've got to prevent the exceptions at the source, and the main way you 
>>> do that for Constraint_Error is to use proper range constraints and null
>>> exclusions on parameters.
>>
>> No. Dynamic constraints cannot prevent anything. They are a part of
>> defining semantics so that violation could be handled elsewhere.
> 
> Sorry, you definitely can prove that dynamic constraints can't be violated.

Only in some cases. For proofs it must be all or nothing.

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

>> Only static constraints can serve prevention. If you let Constraint_Error
>> propagation, you already gave up with static constraints and with
>> provability on the whole class of all instances.
> 
> If you don't want Constraint_Error to propagate (and generally one does 
> not), then you don't put that into the exception contract for the routine.

This would make the routine non-implementable, because, again, you cannot
do that on the callee side. It is a halting problem.

>> You still can have it provable on per instance basis and this is the
>> client's side.
> 
> No, that's making a lot more complicated that it needs to be, and I don't 
> think it's possible in any useful generality.

SPARK does this already. Moreover historically the concept of correctness
proofs was explicitly about instances. Only later, with the dawn of generic
programming, it was expanded onto contracts and behavior in general (e.g.
LSP). The latter is much more difficult and frequently impossible in hard
mathematical sense (undecidable).

> In any case, going that route completely takes the compiler out of the 
> equation. Once you do that, only an extremely limited number of users would 
> care, and there will be no effect on normal programs.

I disagree. I trust that most Ada programmers will enjoy trying it in their
program and gradually relaxing requirements on the proofs as they see what
can and what cannot be proved.

This process would be extremely useful for deeper understanding and
evaluation of how the given implementation works and how software
components interact each other in the concrete case (AKA software
integration).

>>>>>> You can do this only at the client side. Which is why it cannot be
>>>>>> contracted for the callee. When you move from instances to universally
>>>>>> holding contracts you frequently lose provability.
>>>>>
>>>>> ...of things that aren't worth proving in the first place. You get rid 
>>>>> of constraint_errors from bodies by writing good preconditions, 
>>>>> predicates, constraints, and exclusions in the first place.
>>>>
>>>> Really? You can start writing preconditions for +,-,*,/,** defined in the
>>>> package Standard and continue to user defined types and subtypes. If
>>>> anything is totally impractical then the idea to move Constraint_Error 
>>>> from post to pre-condition. It is wrong and will never work for anything 
>>>> beyond trivial examples.
>>>
>>> Which is amazing because it works for most examples. (It doesn't work for
>>> overflow of "*" very well, but that's the only real issue.) And in any case,
>>> there is no point in moving it for language-defined operators -- both the
>>> compiler and any provers know exactly what they do. It's only for
>>> user-defined subprograms that you need to do so.
>>
>> How are you going to do that for user-defined subprograms using
>> language-defined operations, which are all user-defined subprograms?
> 
> Why is there a problem? Every Ada compiler (and pretty much every other 
> compiler as well) does it already.

How do you prove that this does not raise Constraint_Error

   function Geometric_Mean (A, B : Float) return Float is
   begin
       return sqrt (A * B);
   end Geometric_Mean;

> The only issue is that programmers can't 
> harness it for their own purposes. I would hope that exception contracts 
> would be defined in order to do that.

Yes. But they will only help if used on the client side and when bodies are
looked into.

1. You will not prove that sqrt never raises Constraint_Error. You will do
that in *your* calls to sqrt it never does.

2. In a great number of cases you won't be able to contract *when*
Constraint_Error is to be raised. Consider this:

   function Sum (A : Float_Array) return Float;

You cannot spell the contract when Sum must raise Constraint_Error and when
not. Such a contract would much more complex (=> error prone) than the
implementation itself. This is why when the caller of Sum contracts itself
not to raise Constraint_Error, you will have to look into the body of Sum
in order to prove that. Otherwise, you will end up with Java's exception
contracts mess and brainless catch-all handlers.

>>> Huh? This makes no sense for this problem. You can't do that in any 
>>> version of Ada (or any other sensible language),
>>
>> Of course I can. It is MI. Even in Ada it is partially possible with
>> interfaces, just a bit more clumsy than it should be. It is trivial to
>> statically ensure that Write will never be called on Read_File_Type. It 
>> has no such operation.
> 
> But you can't know when you declare a file object what mode it will have, or 
> even if it will get one. That's determined dynamically because by the result 
> of Open.

Nope. Open must be a primitive operation of file type. Readonly file Open
/= write-only Open/Create.

>>> because it would require that the
>>> type of a file object could change in response to operations.
>>
>> Never.
> 
> You've never explained how you supposely static approach would work in the 
> face of failing Opens, among other things.

It is supposed to work with Read and Write.

Maybe I didn't understand your point. I didn't say that Open should not
raise Status_Error. I did that Read should not.

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.

> But you are insisting on more than that, and I think that's actively harmful 
> to programming in general. You seem to insist on access to bodies even with 
> such contracts, but that would prevent all compile-time checking -- the only 
> kind that would benefit most programmers.

I don't see how allowing correctness checks involving the bodies should
prevent correctness checks involving the specifications.

> I want each subprogram to be 
> checked in isolation (subject its contracts), because in that case there is 
> no coupling between calls and bodies.

This will be too weak to be useful. It was attempted long ago by LSP.

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