Hacker News Reader

I agree that termination isn't part of soundness. I was trying to explain how null pointer exceptions are compatible with soundness in Java.

As far as I understand it, Java covariant arrays are sound because the language is defined to throw before the unsound assignment happens. The link I had above claims as much. Maybe I have the definition wrong too?

View on HN

Perhaps you're right there since the check is moved to runtime, I must have glossed over that.

If you look at one of the sibling comments though, it's a bit of a moot point. There's a paper showing a number of unsound bits of code in Java and Scala that use nulls to do pernicious things like transmute types.

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.

Reply on news.ycombinator.com