Re: Securing type extensions

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

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.
An exception is thrown otherwise, or worse.  So both, the programmer
who has written the partial program and the programmer who
has written the plug-in code may have an interest in following the plan.

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?


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

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

So do correctness and type safety make two parties trust
each other with their business?

In a more peaceful setting, the utility function of a business
might include a variable that stands for income that only high
quality software can generate. (Assuming that customers will pay
a higher price for a better product.)

Again, demonstrable correctness and type safety can be turned into
arguments. If correctness and type safety contribute to high
quality, if high quality entails a higher price, and if paying
a higher price expresses trustworthiness, then correctness and
type safety yield trust.

(There are other reasons for larger sums payed, but I'll
ignore them.)

Georg