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

["Randy Brukardt" <randy@rrsoftware.com>]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:hxkln519n179.1kt13z7phxg2f.dlg@40tude.net...
> 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.

Which is why I'm suggesting something built on top of Ada's types for this 
purpose.

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

Again, this is precisely what I'm talking about. SPARK is a disaster because 
it insists that you do everything it's way, or nothing at all. I want to be 
able to incrementally add checks as they become apparent.

The big disconnect is that you (and lots of other misguided people) think 
that types have something to do with operations. Types are more fundamental 
than operations; they get *used* in operations, rather than the operations 
being part of the type. Ideally, a type is nothing but a black box (an Ada 
private type). Operations are the next level of complexity, and exist 
separately from the types.

                             Randy.