Type soundness is always relative to a kind of error that a type system is designed to rule out. So any type system can be made trivially sound by decreeing tha

Type soundness is always relative to a kind of error that a type system is designed to rule out. So any type system can be made trivially sound by decreeing that its purpose is not to eliminate any kind of error. This is why “mathematically civilized” is a much better term. For example, even if you don't mind null pointer exceptions, it is not mathematically civilized to add one extra case to everyone's case analyses.