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.