Re: Securing type extensions

[Georg Bauhaus <rm-host.bauhaus@maps.futureapps.de>]

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


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


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


> 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.
"Contract" is a highly overloaded term, I must refuse to use it in
this context, since I cannot refer to just some isolated technical
set of definitions but must include rules relevant to program
production and use.


Georg