Are Dart and Java type systems sound?

From Dart docs:

Soundness is about ensuring your program can’t get into certain invalid states. A sound type system means you can never get into a state where an expression evaluates to a value that doesn’t match the expression’s static type. For example, if an expression’s static type is String, at runtime you are guaranteed to only get a string when you evaluate it.

Dart’s type system, like the type systems in Java and C#, is sound. It enforces that soundness using a combination of static checking (compile-time errors) and runtime checks. For example, assigning a String to int is a compile-time error. Casting an Object to a string using as String fails with a runtime error if the object isn’t a string.

This is an interesting point of view - yes type system is sound (based on the provided definition), but at the same time it means that the application can crash due to type error 🤔.

For example, if I would write:

1public class HelloWorld{
2    public static void main(String []args){
3        String[] strs = { 1 };
4    }

It will not compile:

$javac error: incompatible types: int cannot be converted to String
        String[] strs = { 1 };
1 error

But this will compile:

1public class HelloWorld{
2    public static void main(String []args){
3        String[] strs = { "1" };
4        Object[] objs = strs;
5        objs[0] = 1;
6        String one = strs[0];
7        System.out.println("Hello World");
8    }

and fail:

$java -Xmx128M -Xms16M HelloWorld
Exception in thread "main" java.lang.ArrayStoreException: java.lang.Integer
	at HelloWorld.main(

I feel like something is twisted here.

Can we say that type system is sound, but static analyzer isn’t?

Or the other way around - if we can say that relying on dynamic type checks is enough to have a sound type system, can we say that Ruby is sound?

11 + "0"
2// TypeError: String can't be coerce into Numeric

See also: Java is Unsound: The Industry Perspective

Except where otherwise noted, content on this site is licensed under Creative Commons Attribution-NonCommercial-ShareAlike 4.0