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

[Mike Samuel]

2010/4/9 Sandro Magi <naasking at higherlogics.com>:
> 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.

I still disagree with the last assertion.
I agree with the first statement but a programming language is also a
tool.  And for any successful language there is a larger audience who
view it as a tool than who view it as a system of axioms.
And the proper names for a consistent set of axioms is "consistent," not "safe."

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

Thank you for explaining.

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

Would you agree with the statement "PHP is memory-safe yet there
exists no specification for it."

>>> 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
>
> _______________________________________________
> cap-talk mailing list
> cap-talk at mail.eros-os.org
> http://www.eros-os.org/mailman/listinfo/cap-talk
>