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

Sandro Magi naasking at higherlogics.com
Mon Apr 12 09:22:40 PDT 2010

On 11/04/2010 1:13 AM, Jonathan S. Shapiro wrote:
>> Then perhaps I misunderstood what you meant by, "but we implement the
>> protection of that abstraction imperfectly". I took imperfect protection
>> to mean the abstraction could be violated resulting in undefined
>> behaviour. This means it's unsafe, and any program exploiting this new
>> abstraction may be able to induce some unpleasant effects.
> My intent was that *if* the new abstraction is violated, then use of
> the new abstraction may not have the intended results, but that
> *other* abstractions are not thereby violated. So it's undefined, but
> within constraints.

Whose intentions are you referring to here? Java's non-strict FP can
have results the *developer* didn't intend when run on a different
architecture. Or is the result not intended by the *spec writer/language
designer*? If the former, it's not a safety issue, if the latter it
might be if it violates some other property required in the spec.

> Concrete example: I suspect we don't have DEFOBJECT quite right in
> BitC. Doesn't violate anything else in the language, but we may not
> have the existential encapsulated in the way that we ultimately need.

That's not unsafe, as long as the spec is consistent, in the sense that
it cannot specify some invariant but provide a way to violate that

For example, if the spec requires that existentials can only be
created/opened using pack/unpack, but some means of opening an
existential other than unpack is available, that would be unsafe.

Your example sounds more like a case of a "bad/inappropriate
abstraction" rather than a safety issue.


More information about the cap-talk mailing list