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

[Sandro Magi]

On 09/04/2010 2:51 PM, Mike Samuel wrote:
>> So does non-deterministic choice, but admitting non-determinism does not
>> by itself make a language unsafe and you have not explained how it
>> could. There are many safe languages with non-determinism.
> 
> I don't quite understand why you think undefined vs undetermined is a
> useful distinction here, and you're still talking about specs.

1. How can you not talk about specs? A programming language is a formal
system wherein you must define the meaning of values and errors, of true
and false, and all the axioms, ie. the primitives, by which one can
construct programs. The whole question of safety is determined by the
properties dictated by the spec.

2. Re:undefined vs. non-determinism, I'm having a hard time
understanding what is so controversial here. These terms have well
understood meanings in computer science, as regards specifications.

Non-determinism simply means the output cannot be predicted solely from
the inputs, but the output is still well-formed (ie. from a known domain).

Undefined basically means "error", usually resulting in a crash or
corruption.

Defining a safe language thus consists of defining inviolable
abstractions via which all program behaviour is expressed. A safe
language can be non-deterministic, but a safe language cannot have
undefined behaviour. Exceptions are typically used to flag conditions
that would normally result in undefined behaviour in an unsafe language.

Thus Java's FP is non-deterministic, as it is classified on the Joe-E
ticket, and not "undefined" which simply does not apply to Java. Java
operations do not result in undefined behaviour which is why Java is safe.

Non-strict FP cannot crash or corrupt the VM, or violate other
abstractions. The non-strictfp abstraction is entirely self-contained
(ie. the domain is known), and the fact that it can produce
unpredictable results makes its behaviour non-deterministic, not
undefined. Threading, non-strictfp, garbage collection timing, etc. are
examples of non-deterministic behaviour, not undefined behaviour.

> (1) We are talking about Pierce's definition of safe.  Not some other
> definition that refers to language specifications.
> 
> (2) The audience of this definition is not just spec writers.
> 
> (3) The definition of "safe" should allow people who have not read the
> language spec to reason about the suitability of the language to their
> goals.

I agree with all of the above, with the caveat to (1) that safety is
inseparable from the discussion of the language spec.

>> 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. 

Firstly, what does "user expectations" mean to you? Because your
arguments so far imply that "Java FP conforms to IEEE754 by default" is
your user expectation. This is exactly the user expectation that is
irrelevant to the question of safety.

I agree that a language should conform to user expectations when those
expectations follow from the operational semantics and axioms of the
language as dictated by the spec. If your language wants to provide
completely random arithmetic, and no other kind, that language is still
safe, though practically useless obviously.

> 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.

If you're back in your strictfp code, then all your values are
guaranteed by the spec to have the proper form. What safety guarantees
do you lose?

Sandro