If we consider a program a state machine, then a sound type system is one that rules out all operations for which the next state is undefined. So Null pointer

If we consider a program a state machine, then a sound type system is one that rules out all operations for which the next state is undefined. So Null pointer dereference is sound in Java. The next state is well defined even if it is just throw a NPE. In C it is not, because there is no well defined next state.