Re: Securing type extensions

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

On Tue, 14 Sep 2010 12:02:28 +0200, Georg Bauhaus wrote:

> I'm asking about visibility and how it can possibly help ascertaining
> that user supplied subprograms are trustworthy---which is, by
> definition, not the same thing as "safe".

Hmm, how "trustworthiness" corresponds to correctness and type safety?

> So I'm speaking about trust and operations not known yet, in the
> presence of user extensible types.

All operations are known. Dispatching call always call a *known* operation,
because a primitive operation is defined on the whole class. What you call
unknown is late binding to a *part* of the body of the operation. It is no
less known as sqrt taken from the standard library and resolved by the
linker. It is separation of implementation and interface, after all.

>   Your_Overriding (My_T'Class (Some_Object));
> 
> Some_Object is of a type that may not exist yet when I write
> the body surrounding the above.

So can the computer, where the program is supposed to run. The category of
developing time is meaningless to the program semantics.

> If so, what is the foundation of trust in this O-O style callback scenario?

See above. It is type safe. It is possibly incorrect. More elaborated
contracts are applied to the *visible* specification, more can be said
about correctness. No difference to sqrt, BTW.

> I'm asking for the degree to which Ada's ___, ___, ... can establish
> trust. That's not the same thing as those purely mechanical static
> safety properties of programs.  It is what human parties rely on when
> calling user supplied prim ops with LSP enacted in some event
> driven parser, for example.

Let us not go into a discussion why LSP does not work. If you want to be
sure about substitutability it is better to call it so, because LSP is
misleading, inconsistent and wrong.

So, a member of a class is *always* substitutable for an operation defined
on the class. You cannot find anything more here without going into
contracts beyond mere types. Ada stops here and this is unspecific to
dispatch. So see above. SPARK has to tell more.

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