[cap-talk] definition of the term "safe language"

[Mike Samuel]

2010/4/6 Matej Kosik <kosik at fiit.stuba.sk>:
> Friends,
>
> I was delighted to find a clear definition of the term
> "safe language" in this book:
> http://www.amazon.com/Types-Programming-Languages-Benjamin-Pierce/dp/0262162091/ref=sr_1_1?ie=UTF8&s=books&qid=1270548760&sr=8-1
> According to Pierce:
>
> "a safe language as one that protects its own abstractions.
> Every high-level language provides abstraction of machine services.
> Safety refers to the language's ability to guarantee the integrity
> of these abstractions and of higher-level abstraction introduced
> by the programmer using the definitional facilities of the language.
> For example, a language may provide arrays, with access and update
> operations, as an abstraction of the underlying memory.
> A programmer using this language then expects that an array can be
> changed only by using the update operation on it explicitly---and not,
> for example, by writing past the end of some other data structure.
> Similarly, one expects that lexically scoped variables can be accessed
> only from within their scopes, that the call stack truly behaves like a
> stack, etc.
> In a safe language, such abstraction can be used abstractly;
> in an unsafe language, they cannot: in order to completely understand
> how a program may (mis)behave, it is necessary to keep in mind all sorts
> of low-level details such as the layout of data structures in memory
> and the order in which they will be allocated by the compiler.
> In the limit, programs in unsafe languages may disrupt not only their
> own data structures but even those of the run-time system;
> the results in this case can be completely arbitrary."
>
> I hope you like it as much as I did. :-)
>
> The term "object-capability language" may then be a hyponym of the term
> "safe language".

It's a great definition, but is it ocap language really a hyponym of
it?  I would think the definition of an ocap language would only hinge
on the safeness of the language abstractions necessary to preserving
ocap invariants.

For example, a language that is safe w.r.t. object references, scopes,
and ambient authority but also had abstractions such as
    x := y after 5ms
to simulate signal propagation in circuits a la Verilog would be an
object capability language regardless of whether the delayed
assignment to x happened before the assignment to y in the below
    x := y after 1 ms
    y := z after 1 ms

cheers,
mike


> _______________________________________________
> cap-talk mailing list
> cap-talk at mail.eros-os.org
> http://www.eros-os.org/mailman/listinfo/cap-talk
>