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: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. 
Ada compilers do it all the time. The issue is letting the programmer have 
access to that information.

> 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. 
Hardly ever would you want that in the contract.

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

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.

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

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

>> 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. That's because it wouldn't work 
at all.

>>>> One thing we had to do is to make these things work is to allow 
>>>> existing
>>>> compilers to use runtime checks, with the hope that more will become
>>>> proved over time. Compiler technology isn't quite ready for mandatory 
>>>> proof
>>>> requirements (maybe next time).
>>>
>>> This is a conflation of its worst.
>>
>> Carried over from Ada 83. Ada will never be a language that requires much 
>> in
>> the way of proof, it would be way too disruptive to existing
>> implementations.
>
> I don't see how adding optional exception contracts should disrupt
> anything.

It wouldn't, and I hope we'll do that. But that doesn't have a darn thing to 
do with our discussion; I'm assuming such contracts (and global contracts) 
exist -- else absolutely nothing can be done. Everything I've been talking 
about for weeks is for Ada 202x, which certainly will have exception 
contracts if I have anything to do about it.

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 want each subprogram to be 
checked in isolation (subject its contracts), because in that case there is 
no coupling between calls and bodies.

                                     Randy.