Re: Securing type extensions

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

On Tue, 14 Sep 2010 23:18:36 +0200, Georg Bauhaus wrote:

> On 9/14/10 2:22 PM, Dmitry A. Kazakov wrote:
>> 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?
> 
> I'd consider the relation of trustworthiness, correctness and type
> safety at least from two viewpoints, a technical one and one on
> conflict:
> 
> 1 - Technically, a program may have certain formal properties,
> such as no type errors. (Like a program can suffer if written
> in Python).  Each formal property may exclude precisely the
> corresponding class of errors, if there is such correspondence.
> 
> Suppose a partial program has "sockets" into which foreign code
> can be plugged, to make it complete.  Such as a type extension
> with overridden subprograms.  The completion is done on site.
> At the very least the interfaces must match.
> 
> But the parent type's "plan" might require that the type's operations
> be called in a certain order, sayoperation A
> is called before operation D, no matter what comes in between.

This is poor design. Abstract types were introduced in first place in order
not to have such uncheckable low-level contracts. One of the ideas of OO
decomposition was to introduce objects maintaining their state in order to
simplify interfaces.

> 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. If you have contracts to be checked
dynamically, you need a meta framework where contracts were types,
statically known. Something must be static.

> 2 - The utility function of a business might include a variable
> that stands for cost of conflict. Cost of conflict is in part
> negotiated, in part a consequence of the legal system.
> 
> 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. The solution is
specifications/contracts. More detailed they are less space is left for
conflicts.

> Demonstrable correctness and type safety can be turned into
> arguments. "Clearly, our partial program is correct, and type
> safe.  Therefore, your type extension makes the product
> malfunction." -- "But we only varied the order of calls and
> your type specifies nothing in this area.  Why didn't you
> specify ordering requirements as preconditions?" ...

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?

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