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

[Jonathan S. Shapiro]

It does not sound better. Pierce's definition of language safety is
setting context for his book. In the context of the book, this is what
he wants the term "(unqualified) language safety" to mean. Once we
step outside the book, I don't think there is general agreement about
the definition, which is the heart of the problem with the
conversation here.

What Pierce chooses to bundle under the heading of language safety is
a number of properties concerning the well-defined behavior of the
language operational semantics plus some related properties that are
necessary preconditions to well-defined behavior. This is a very fine
set of properties indeed for a language to obey, so I am not for a
moment disputing the merit of the properties he has chosen. I'm merely
disputing his monopoly on the definition of language safety.

Now. If we, collectively, in this thread, choose to accept
"Pierce-safety" as our working definition of "(unqualified) safe
language", I'm perfectly content. We just need to be clear when we
talk to others that we are adopting a local concensus that may not be
accepted elsewhere without explanation. In this case, because Pierce
is so widely read, it's actually a pretty widely shared local
consensus. That alone may be a good reason to accept it.

shap

On Thu, Apr 8, 2010 at 2:07 PM, Matej Kosik <kosik at fiit.stuba.sk> wrote:
> Jonathan S. Shapiro wrote:
>> Generally speaking, the term "safe language" has come to
>> be a synonym for "type safe language".
>
> Pierce explicitly disagrees with this viewpoint:
>
> "Language safety is not the same thing as static type safety. Language
> safety can be /achieved/ by static checking, but also by run-time checks
> that trap nonsensical operations just at the moment when they are
> attempted and stop the program or raise an exception. For example,
> Scheme is a safe language, even though it has no static type system.
> ----
> Conversely, unsafe languages often provide "best effort" static type
> checkers that help programmers eliminate at least the most obvious sorts
> of slips, but such languages do not qualify as type-safe either,
> according to our definition, since they are generally not capable of
> offering any sort of /guarantees/ that well-typed programs are well
> behaved--typecheckers for these languages can suggest the presence of
> run-time type errors (which is certainly better than nothing) but not
> prove their absence."
>
> Alternatively, I could formulate the distinction in the following way:
> The difference between safe and unsafe languages is that programs
> written in safe languages are (tractable) mathematical objects whereas
> programs in unsafe languages are not (tractable) mathematical objects.
>
> Does this sound better?
> _______________________________________________
> cap-talk mailing list
> cap-talk at mail.eros-os.org
> http://www.eros-os.org/mailman/listinfo/cap-talk
>
>