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

[Jonathan S. Shapiro]

On Fri, Apr 9, 2010 at 4:58 PM, Mike Samuel <mikesamuel at gmail.com> wrote:
>>> Undefined basically means "error", usually resulting in a crash or
>> corruption.

Replace "usually" with "hopefully". Undefined leaves the implementor
complete leeway. It's the very fact that it *doesn't* reliably cause
an error that is the source of the problem.

Consider, as a concrete example, that the behavior of unspecified bits
in the Pentium specification has been an ongoing source of evolution
problems for the architecture. S/360->S/390 did not suffer this,
because it had no such bits. There were reserved bits, but no
unspecified bits, and no reserved bits whose specified requirements
were unchecked.


>> I agree with all of the above, with the caveat to (1) that safety is
>> inseparable from the discussion of the language spec.
>
> Would you agree with the statement "PHP is memory-safe yet there
> exists no specification for it."

Certainly not. First, in the absence of specification, there is no
such thing as PHP. There are only implementations of PHP. Second, in
the absence of specification, there is only *alleged* safety sustained
by strong assertion. That isn't safety.

>>>> That Java's default does not conform to user expectations, and is in
>>>> fact non-deterministic, is irrelevant. It was a poor design choice, but
>>>> it is not unsafe.
>>>
>>> Nonsense.  The point of Pierce's definition *is* that the failure of a
>>> language to conform to user expectations is what makes it unsafe.

Not quite. User's don't dictate language design in Pierce's view. The
user's valid expectation is that the language specification will tell
the user what there expectations should be in all circumstances
provided that the program is well-formed and well-typed (either
statically or dynamically), and that no behavioral expectations will
be "left out". The defined behaviors must be consistent; they need not
be sensible or useful.

>>> That there exists a subset of the language that is safe does not
>>> render the entire language safe.  If I call out to any libraries that
>>> use unstrict fp, then I lose all the safety guarantees.

Mechanisms for call-out to unsafe code are a pragmatic compromise. Any
program using these mechanisms is no longer checkably safe. Depending
on what the unsafe mechanism is, this may or may not invalidate the
underlying safety properties of the whole program. For example, the
use of pointers in C# is generally unsafe (which is unfortunate,
because many such uses are perfectly okay and checkable).

As a general exception, we allow such call-outs to bits of trusted
code supplied by the runtime system that perform well-specified
actions, and we distinguish this from call-out to arbitrary code.


shap