Re: Securing type extensions

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

On Wed, 15 Sep 2010 22:47:51 +0200, Georg Bauhaus wrote:

> On 9/15/10 10:15 AM, Dmitry A. Kazakov wrote:
>> On Tue, 14 Sep 2010 23:18:36 +0200, Georg Bauhaus wrote:
> 
>>>> Hmm, how "trustworthiness" corresponds to correctness and type safety?
> 
>>> 1 - Technically, [...]
>>> But the parent type's "plan" might require that the type's operations
>>> be called in a certain order,
>>
>> This is poor design.
> 
> Certainly, and a "plan" suffices as an example, if you agree
> that perfect technical specifications of what (again, just for the
> sake of an example) a type writer expects an extension writer to
> do are not always possible. (Which I understand you do.)

That is not the type writer. There are three parties, the interface
designer, the designer of an implementation and the user of the interface
(class). Since it is the last two, who must get along, class-wide
implementations do not really change anything in the picture.

>>> How do you talk about this on site?  Can you trust the plug-in code?
>>> Suppose you don't use Ada, but Python or some other more dynamically
>>> typed language. Can you  even assume the type has the same interface
>>> as its parent? When the absence of a statically known interface
>>> destroys all hope for type safety, how can programmers sill trust
>>> Google to continue providing meaningful Python objects for Google
>>> App Engine?
>>
>> This is an unrelated issue.
> 
> The issue is related to trust, and to type extension, and it is an
> existing challenge.
> Call it poor design on the part of Python framework writers, if that
> is what it seems to be.   But since the framework exists as a foundation
> for real software, it does affect multi-party work. We can't always
> control the parent types, and must see if we can find it trustworthy.

and the point is? 

>>> The conflict here is triggered by a malfunctioning program:
>>> who/what is to blame when a type extension (by party X) does not
>>> work nicely with a partial program (by party Y)?
>>
>> Any software/hardware decomposition has this problem.
> 
> Yes.  The composition problems are varied, though.
> One language can offer more help than another.

One like SPARK.

>> The program semantics cannot be specified exhaustively. I don't know were
>> you want to go, but it is not only impossible to specify all program
>> semantics, moreover, it is also impossible to have LSP subtyping.
>> Substitutability in the context of subtyping cannot be upheld statically.
>> You have to verify substitutability per each case of substitution.
>>
>> Since we trust you, we do not verify it. Is it what you consider as
>> "trustworthiness"? Non-contracted behavior?
> 
> More inclusively, a mix of technical and social properties of
> a software situation will lead to more or less trust.

The way you described it, trust has no physical meaning. It is a
psychological phenomenon, not a subject of CS and SW engineering. Maybe a
greater effect in gaining trust could be achieved by painting green walls
of the cubicles, by writing "no gene-modified bits inside" on the DVD
cover. Whatever...

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