[e-lang] LockBox and static typing (was: Newbie Joe-E questions)

[David Wagner]

Toby Murray writes:
>In E, this implementation would be vulnerable to malicious (supposed)
>LockedBoxes stealing Tokens. I'm wondering, does the Java static type
>system prevent this sort of problem?

No, it doesn't prevent that sort of problem.

I should have mentioned that you shouldn't use my Lockbox example for
anything real; it's a lame expository example thrown together off the
top of my head without any real thought put to it, and intended only
to illustrate a particular point.  If you want to build something for
real it's probably better to instead use a Sealer/Unsealer/Brand that
someone has put some thought into and that has been reviewed (see, e.g.,
the implementations that Tyler has built in Waterken).  Sorry that I
failed to include that disclaimer in my original email.

As David Hopwood points out, one serious flaw in the Lockbox example is
that the Lockbox class is not marked as final.  There may be other
flaws as well.

If the Lockbox class were marked final, then you could presumably
convince yourself that the particular implementation of Lockbox.unlock()
doesn't actually retain tokens, by reviewing the code.  Even better, if
the Lockbox class were marked as final and Immutable, then I think you'd
be able to have some confidence that Lockbox.unlock() doesn't retain
stolen tokens, because the unlock() method would not have access to any
mutable state where it could preserve those tokens after it returns.
In the latter case the Joe-E static type system would be helping (by
reducing the burden on code review).