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

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

On Thu, 11 Jul 2013 17:28:31 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:1s6sw93u97355$.1n0205ucj6251.dlg@40tude.net...

>> How do you know that the copy you made is authentic? What is about the 
>> accuracy of the implementation?
> 
> That's easily determinable by unit tests (which are needed in any case - 
> testing and proof are not exclusive, you need both because it's real easy to 
> prove the wrong thing).

Firstly, you propose to replace proofs with tests, which automatically
disqualifies the answer.

Secondly, it does not work anyway. One famous example was given by Forsythe
in his book on numerical methods. It is solving quadratic equation using
school formula. In some cases (when roots are close to each other) the
accuracy catastrophically drops for one root and increases for another. You
*cannot* catch such stuff through tests. Only analysis can, and analysis is
equivalent to proofs.

>>>>> What's too hard shouldn't be bothered with, because we've lived just
>>>>> fine with no proofs at all for programming up to this point.
>>>>
>>>> We didn't. Accessibility checks and constraint errors are a permanent
>>>> headache in Ada.
>>>
>>> Constraint_Errors a headache? They're a blessing, because the alternative 
>>> is zillions of impossible to find bugs.
>>
>> No, the alternative is to prove that the constraint is not violated.
> 
> That's completely impractical.

You *always* can do on the client's side:

exception
   when Constraint_Error =>
       Put_Line ("Oops!');
end;

Which is the point, things are much simpler on instances of use compared to
universal usage.

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

> If for whatever reason you can't do this, then yes you lose proveability.

Nope. See above. I can prove that Constraint_Error is handled by given
client. Which is what Ada programmers really want, because unhandled
Constraint_Error is by far the most common bug.
 
>> Note how accessibility checks attempted in the form of a contract became
>> more problem than solution. In order to have it provable you must
>> strengthen it. Probably every Ada programmer was annoyed by silly "must be
>> statically deeper" messages about pointers. It cannot be handled at the
>> level of contracts. Yet in most cases it is no problem to see that a
>> *given* pointer is never dangling.
> 
> "No problem"? Informally, sure. It's impossible to prove in any real case; 
> there is too much going on. (Claw, for instance, prevents it by design, but 
> I don't think there is any way to formally describe that design -- certainly 
> not in systems like Spark which ignore the effects of finalization [which is 
> how Claw guarentees non-dangling]).

Most real cases are about downward closures and stuff when pointer is
aliased argument. For the latter you need the body.

>>> It's annoying that one can't tell between specification errors that should
>>> be contracted and proved away and those that are truly runtime (that is, 
>>> a normal part of the implementation);
>>
>> That was ARG's decision for Ada 2012, wasn't it?
> 
> No, it was an effect of Ada 83, which conflated those uses of exceptions. We 
> had to formalize existing practice (we need the ability to add these 
> specifications to existing code without changing any behavior). It would be 
> better for exceptions that we would want to "prove-away" (like Status_Error 
> and Mode_Error in Text_IO) to be strictly separated from those that are 
> purely runtime behavior (like End_Error and Device_Error).

This has nothing with that.

Status_Error and Mode_Error are there because file type as designed does
not reflect its mode:

   type Read_File_Type is ...
   type Write_File_Type is ...
   type Readwrite_File_Type is Read_File_Type and Write_File_Type is ...

Done.

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

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