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

[Mike Samuel]

2010/4/9 Sam Mason <sam at samason.me.uk>:
> On Fri, Apr 09, 2010 at 11:51:05AM -0700, Mike Samuel wrote:
>> 2010/4/9 Sandro Magi <naasking at higherlogics.com>:
>> > 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.
>>
>> Nonsense.  The point of Pierce's definition *is* that the failure of a
>> language to conform to user expectations is what makes it unsafe.  You
>> might not like his definition, and your definition may be better in
>> many ways, but asserting that his definition is not what it is is
>> silly.
>
> I think maybe you're using the term "safe" in place of "good design".  A
> well designed language will *tend* do the "right" thing more often than
> one that isn't well designed.  However, this has very little to do with
> whether a language is "safe" or not.  I'm unsure how to explain this any
> better than has already been done by Sandro or Shap.

I agree that a well-designed language will be safer than a poorly
designed language with the same goals as long as we restrict
discussion to high-level languages where abstraction is a goal.

But there is a legitimate tradeoff between safety and other concerns.
The python community has made a conscious choice in some cases to
allow broken abstractions, because programmers "should know better."
That is a fine choice -- allow the language to admit programs that
break abstractions because other programs benefit from implementations
having the extra wiggle room.


>> 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.
>
> This statement doesn't agree with my understanding either.  If a
> language has "type safety" then that should not depend on whether the
> floating point operations are behaving deterministically or not.  The
> *correctness* of my code certainly may well depend on the FP maths doing
> as I expect, but this isn't a safety issue either.
>
> I think what's happening is a conflation of various technical terms.
> Language level "safety" is the lowest set of invariants that exist
> in a piece of code.  The safety of the abstractions exposed by the
> programming language make it easier to determine whether a body of
> code implemented in this language is "correct".  How "well designed" a
> language is determines how much of the spec a person writing this code
> has to read in order to produce correct code.  Note that for somebody
> to actually determine whether a piece of code correctly implements the
> specified behavior they must know the entire language specification as
> well as the definition of the problem being solved.  It's thus much more
> work to verify code than to write it, but this process is simplified by
> the existence of the safety guarantees provided by the language.

I agree with all of this.
But it is much easier to write generic code in a language that does
preserve abstractions across all programs.

E.g. java (in the sense of language + libraries) exposes a broken
abstraction, equality.  It's broken because it assumes a contract
between equals and hashCode that is not enforced for all possible
programs.  This doesn't cause a lot of problems in practice, but it
means that collection implementors and generic library function
implementors have to bear the burden of limiting worst case behavior
when given Objects that violate hashCode and equals.  Similarly for
implementing sort in the face of broken comparators.


> I hope I've got that about right!
>
> --
>  Sam  http://samason.me.uk/
> _______________________________________________
> cap-talk mailing list
> cap-talk at mail.eros-os.org
> http://www.eros-os.org/mailman/listinfo/cap-talk
>