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

[Sandro Magi]

On 09/04/2010 1:03 PM, Mike Samuel wrote:
>> Just because Java does not provide a floating point abstraction that you
>> expect does not make it unsafe.
> 
> Not according to your definition perhaps, but according to Pierce's it does.
> Java's floating point abstraction admits undefined behavior.

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.

Let's try a different tack: consider a distinct non-deterministic
abstraction. Introducing this abstraction to a language does not by
itself make it unsafe, as the existence of non-deterministic safe
languages demonstrates.

Now introduce an explicit conversion between this non-deterministic
abstraction and a deterministic abstraction. No unsafety was introduced
because the conversion is explicit, so the user specifies which
abstraction he is using. Once again, safe non-deterministic languages
demonstrate that one can convert between deterministic and
non-deterministic abstractions without losing safety.

The strictfp annotation is exactly this conversion. So exactly where
does the unsafety creep in? You might argue that the conversion is
actually implicit and that's where it creeps in, but the choice of
abstraction is in fact explicit as an annotation on the function signature.

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.

> Programmer cannot rely on it to have properties essential to writing
> robust code, but have to do a lot of extra work to only use it in
> certain ways.

What Java does is provide two abstractions, platform-agnostic floating
point via strictfp, and assuming it behaves as you've described, an
abstraction that interoperates with FP but which has a non-deterministic
input. rand-FP is simply another abstraction with  built-in
non-deterministic choice, and you specify which to use with the strictfp
annotation.

strictfp code cannot affect the operation of non-strictfp code except
via an explicit strictfp conversion by parameter passing. The
abstraction boundaries are protected.

I clearly haven't done a good job communicating the reasons why it's
safe, and when I have a bit more time I'll more carefully address
David's e-mail to clarify the confusion I've caused.

> That difference between having to carefully limit the way you use an
> abstraction so you maintain the properties necessary for
> robustness/correctness/etc., and having an abstraction that always has
> those properties, is the core difference between safe and unsafe.

That's the difference between a good abstraction and a bad abstraction.
An abstraction whose invariants are protected is the defining
characteristic of safety. Whether the abstraction is sensible is irrelevant.

Floating point in non-strictfp mode specifies fewer invariants, but as
long as the properties it requires are protected, then it is safe. If
you want an even safer abstraction, ie. even more protected invariants,
then choose strictfp.

Finally, note that compile-time constant expressions always use strictfp
behaviour, so your loop/array example will always produce the same
results. Also note the Peirce specifically includes Java as a safe
language in his book, on the exact same page as the definition Matej
provided, so don't just take my word for it.

Sandro