[danbruc]

That is certainly true, but the point was whether nullabilty has any bearing on soundness. I just tried to argue that the fact that a reference may be a null reference does not (necessarily) defy soundness - the compiler guarantees that you get an instance or a null reference and that is exactly what happens at runtime.

[catnaroek]

If you take the view that object references are options, then it's plain unsound to manipulate object references as though they weren't options! `NullPointerException` is just a dynamic plug on a static type safety hole.

This blog post (I'm not the author) explains the issue (item 3) very well: http://www.sebastiansylvan.com/post/language-design-deal-bre...

[danbruc]

Maybe I (or you or both of us) have a wrong understanding of soundness. I understand it as follows - the specification of a programming language (or its implementation) is sound if the guarantees made a compile time hold at runtime for all inputs. The guarantee for calling a method on a reference in Java is that you either invoke that method or a NullPointerException gets thrown in case the reference is a null reference.

After thinking about it again, unless you made an error in the specification or implementation, every programming language should actually be sound. You can always weaken your guarantees until they (trivially) hold at runtime. But that actually worries me a bit, soundness suddenly seems not such a useful concept. Maybe because I am wrong with my understanding?

Note that this also possibly contradicts what I wrote previously, I may not have thought carefully enough about some of the things.

[catnaroek]

> After thinking about it again, unless you made an error in the specification or implementation, every programming language should actually be sound. You can always weaken your guarantees until they (trivially) hold at runtime.

That's technically correct. But it's like the joke about the mathematician who can only provide technically correct but otherwise totally useless answers.

> But that actually worries me a bit, soundness suddenly seems not such a useful concept.

Indeed, if you define soundness that way, it's a useless concept. That's why I refuse to accept a semantics that doesn't match how programmers actually think about their programs. I consider it undefined behavior to dereference a null pointer: the language implementor might trap the error to make debugging easier, purely out of goodness in his heart, but the program itself remains meaningless until it doesn't dereference null pointers anymore.

> Maybe because I am wrong with my understanding?

Nope, you're not wrong.

[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.