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

Matej Kosik kosik at fiit.stuba.sk
Wed Apr 7 11:08:23 PDT 2010


Mike Samuel wrote:
> 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

I am sorry. I do not understand. Do you have in mind some ocap language
that is not safe (according to the Pierce's definition)?


More information about the cap-talk mailing list