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:1rjye7dyn3vgk.66fbcca9y4zd.dlg@40tude.net...
> 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.

Yes, that's precisely what I'm talking about - some sort of exception 
contract. But those don't depend on the kind of constraint.

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

As you showed a couple of days ago, it's trivial on the callee side (just 
stick in a handler). The hope is to use proof techniques to reduce the cases 
where that's required, but I see no important reason to worry about 
eliminating that.

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

Exactly my point! :-)

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

Certainly, there is lots of stuff that's not worth proving that's not 
provable. So what? We've lived for decades without general proof and there 
is absolutely no evidence that general proof would do anything to improve 
the quality and timelyness of software. (Software that takes longer to 
develop isn't viable no matter how much better quality it actualy is.)

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

No one is going to run extra tools beyond compilation; they simply don't 
have the time. The "win" with Ada is that the extra correctness brought by 
the language comes for "free", 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.

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

You can't, because it does. :-) Your contract is not strong enough, which is 
not surprising: you have unbounded types here -- you can prove nothing about 
such types.

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.

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

You might be right, but in that case we're wasting our time even thinking 
about proof, because any technology that requires programmer-visble access 
to bodies is evil. ("Evil" here being a shorthand for "has a bunch of bad 
properties", which I've previously outlined.) And you may say that many Ada 
compilers have such features, and I repeat that pragma Inline and 
macro-expanded generics are evil, if they have any programmer-visible 
effect. Those sorts of things are only acceptable if they are completely 
semantically invisible, and that is rarely true.



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

You don't have to. A properly written Sqrt has a precondition, and that 
precondition raises Constraint_Error when it fails. Sqrt itself never raises 
any exception. You then prove at the call site that the precondition is met.

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

Yup, if you think that *everything* can be contracted and should be 
contracted, the only possible result is Java's mess. That's perfectly clear, 
because I certainly agree with you that you can't explain why exceptions are 
raised formally in many cases. And that's actually OK, because the point is 
to get rid of the exceptions (with smart use of constraints, predicates, and 
preconditions). If you can't do that, there's really nothing to prove and 
nothing to be gained from the contracts.

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

I agree with that, that's the precondition's job.

> 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; 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 -- so your scheme means that the 
file type has to change dynamically during it's lifetime. That's the purpose 
of a subtype, not of a type (in Ada terms, at least).

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

Because you can't have "correctness checks" involving bodies that don't 
exist. And having them depend on bodies is "evil", because it means that a 
change to a body can make a call in someone else's code fail. That's 
completely unacceptable - it would be impossible to write any reusable code 
in such an environment.

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

LSP is a dynamic thingy, completely uncheckable at compile-time.

And you may be right, in which case any sort of proof is worthless, because 
violating encapsulation instantly causes all of the bad effects that Ada 
have been designed to avoid -- changing an unrelated thing (and every body 
is unrelated in Ada terms) never makes someone else's code illegal.

                                Randy.