Re: A broken brand?

On Mon, Mar 3, 2008 at 5:31 AM, Mark Miller <[email protected]> wrote:
> On Mon, Mar 3, 2008 at 3:13 AM, Ben Laurie <[email protected]> wrote:
>  >  >  Depressingly, none of the following tools would have helped:
>  >  >
>  >  >  a) conventional static type checking
>  >
>  >  Wouldn't static type checking have shown that the box() function
>  >  passed was not the one handed over in the first place?
>
>  Yes, which would have prevented intermediation. When this is not
>  contrary to intention, that's fine, and enables Ping's pattern.

A further clarification on my initial reaction:

Type checking would indeed have prevented the attack (at some loss of
expressiveness that would typically have been fine).

However, what I meant by my initial reaction is that type checking
wouldn't have helped *detect* the bug. I don't see a way to have
employed a type system so that MarcS pattern with the bug fails to
type check but without the bug passes the type check. AFAICT, this is
true even for fancy type checking systems explicitly constructed for
reasoning about side effects. However, I have no deep understanding of
these. Could someone who does please comment? Thanks.

David, would MOPS have helped?

-- 
Text by me above is hereby placed in the public domain

    Cheers,
    --MarkM