Is there a difference between type safety and type soundness?

Question

I've been trying to tease apart the definitions of type safety and type soundness and I'm having a heck of a time of it. I asked a professor recently and after a bit of thought he said that there really wasn't any difference. However after reading this it seems like:

• Type Safety is a property of the language that says that the application of functions (and operators) to data is meaningful (i.e. 1 / "Hello" is nonsense and is disallowed)
• Type Soundness is a property of a type checking system that guarantees that its static type predictions are accurate at run time.

This is clearly just a single persons notes and I'm wondering if there is some standard within the PL community. I've done some searching and I haven't found a satisfying answer.

Answer 1

Type safety and type soundness are synonyms in most theoretical work. Type soundness is often formulated with respect to an operational semantics as (type) preservation and progress. Preservation states that if an expression has some type, then after a step of evaluation (via the operational semantics), the resulting expression can be given the same type. Progress states that if an expression is not a value, i.e. it is not fully evaluated, and it is well-typed, then it can be further evaluated.

"Type safety" and "soundness", but particularly "type safety", are also widely used by the (non-theoretical) programming community often in vague, ambiguous, or outright incorrect ways. For example, an API that uses enumeration types instead of allowing arbitrary strings when only a subset are meaningful, say, might be referred to as being "more type safe", but this statement doesn't make sense using the theoretical definition of "type safe" which is a binary property of the language as a whole.