[trurl]

> There does not seem to be any equivalent of the notion of soundness in the world of dynamic typing. However, we can still talk about whether a dynamic type system strictly enforces type safety.

My understanding is that there are well understood definitions of soundness for dynamically typed languages. The soundness theorem will generally be weaker ("your program will evaluate to a value or abort on a type confusion") but it is certainly possible to be sure a given dynamically typed language definition will never make mistakes like confusing an integer for a pointer. Though in the scheme of things such theorems are not much weaker than what you get for a statically typed language with exceptions ("your program will evaluate to a value with the given type or throw some exception").

[naasking]

It actually is significantly "weaker". You make the wrong analogy when you say the dynamically typed case maps to a statically typed one with an exception (which presumably is a value in your language).

The correct analogy is to a segfault, meaning the program exited abnormally because it's inconsistent in an important way. It's the reason statically typed languages are faster than dynamically languages: expressions have a fixed meaning than enables optimisation guarantees you can depend on.

[kd0amg]

That is a "soundness theorem" and maybe even a "[static] type soundness" theorem (if you like the word "unityped"), but the point is that's not really saying anything about conclusions drawn by the classification of values into dynamic types.