[wisam]

I thought soundness (when it comes to statically-typed languages) means that the static type checker won't pass a program that would raise runtime type errors. Your comment (and Dart's website) was the first time I've read a claim of soundness by combining static type checker and runtime checks. Doesn't your definition mean that most type systems (even those of weakly and dynamically-typed languages) are sound. Even JS and PHP will eventually give up and give you a type error. Can't think languages other than C (which might give you segfaults or whathaveyou) that won't fit that definition of soundness.

Sincere question, what am I getting wrong?

[munificent]

"Sound" is one of those words whose definition varies more than you think. Some people use it to mean only statically proven to be free of type errors.

But, I think in practice, most languages that we call "sound" do indeed rely on some amount of runtime checking in order to guarantee that. Java and C# are both widely considered sound — and need to be to preserve memory safety! — and they both use runtime checking to ensure that (on cast operators and covariant array usage). I think even Haskell defaults to runtime checking of non-exhaustive pattern matching, which could be considered a form of "type errors".

> Doesn't your definition mean that most type systems (even those of weakly and dynamically-typed languages) are sound.

Dynamically-typed languages detect the type error right at the point where you try to perform an invalid operation for that type. They are safe in that that doesn't generally lead you into a hard crash or scary undefined behavior.

C# and Java are similar with respect to array usage — you get the type error right when you attempt to do a covariant store. Dart is similar for covariant generics.

But in most other cases, Dart detects the error earlier, at the point that you attempt to cast a value to the wrong type, not when you later use it as that wrong type.