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

[Matej Kosik]

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?