[catnaroek]

> Maybe I (or you or both of us) have a wrong understanding of soundness.

I'm using my own interpretation of “soundness = progress + preservation”, originally due to Wright and Felleisen. “Progress” means “not getting stuck” (a term is either in normal form or further reduces). “Preservation” means that, if a term `t` has type `T` and reduces to a term `u`, then `u` also has type `T`.

From a purely technical point of view, raising a NPE is a well-defined execution step, different from getting stuck. But I contend that this is just a technicality, and not really how a programmer thinks about his code. For practical purposes, in most situations, throwing a NPE is reaching a stuck state, and thus a violation of type safety.

[danbruc]

Which then brings us all the way back to the first comments - without agreed and accepted definitions statements about programming languages may be way more up for interpretation then one hopes.