Re: Seeking for papers about tagged types vs access to subprograms

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

On Sat, 11 May 2013 09:06:11 +0200, Georg Bauhaus wrote:

> On 11.05.13 08:37, Dmitry A. Kazakov wrote:
>> First of all, there are preconditions of operations and the precondition
>> put on individual calls. I don't know which one you mean here. But the
>> preconditions of operations must be statically true. Meaning: a declared
>> operation can be called anywhere. The client may annotate his calls to the
>> operation with additional preconditions related to the logic of the program
>> that uses the operation. These are not the property of the operation and
>> unrelated to the type.
>>
>> The idea that the precondition of first kind should depend on the state of
>> the objects involved in the operation is a very, VERY bad idea.
> 
> How do you specify the preconditions of the second kind (on individual
> calls) in such a way that a programmer, wishing to calling these operations,
> ensures the calls won't fail as a consequence of violating these
> preconditions?

"Fail" is a wrong word here. The right wording is ensuring postconditions.
That is completely unrelated issue, IMO.

I have a feeling that people confuse typing with this, which is basically
program correctness en large. You cannot ensure program correctness through
types. And since full correctness proof is unachievable anyway I want to
separate it from types.

Second kind checks (e.g. SPARK) should be optional so that the programmer
would add or remove checks depending on requirements and provability. 

Especially because there is also a big difference in the design of type
checks and correctness checks. We design types top-down, at least the most
important ones. Type design is frequently irreversible, few things can be
changed later without big troubles. It is almost waterfall. On the
contrary, the correctness checks are bottom-up. You probably never get to
the top. But you can well figure up essential things at the bottom for
which it were possible and desirable to check things statically.

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