Copy/pasted from google search: > A sound type system means you can never get into a state where an expression evaluates to a value that doesn't match the expr

Copy/pasted from google search: > A sound type system means you can never get into a state where an expression evaluates to a value that doesn't match the expression's static type. It's not actually that hard to make a provably sound type system. The claim can only strain belief if it includes some type-level feature that makes this difficult. Of course, it should also be proved. e.g. Java's type system is not sound even though there is no good design reason while it shouldn't be (to be fair - it only happens in cases so intricately twisted that nobody will ever stumble on them by accident).