[cap-talk] Midori in The Register

[Jonathan S. Shapiro]

On Wed, 2008-08-06 at 06:39 -0700, Mark Miller wrote:

> If I understand what Ben means by 
> > It can be *circumvented*, but if the coder does not go
> > out of his way to do so, the code is *effectively* type-safe.
> [emphasis added]
> then I'd classify it as type unsafe.

I understand your point, but I think we want to be a little careful
going down this path. In effect, Apache is implemented in a thin
meta-language over C that is intended to be safe. I concur that the
implementation doesn't achieve the goal, but let me pose two challenges
to the argument you are making:

  A C program that is successfully checked by some checker imposing
  stronger guarantees than C ensures can be type safe, even though C as
  a language does not structurally ensure safety.

  A statically compiled ML program is generally considered safe, even
  though a user could link arbitrary ASM code into the binary and
  execute that. Also the ML runtime is written in an unsafe language.

My point is only that the term "safe" should not be interpreted to apply
only to programs that are safe by virtue of structural language
constraints.


shap