A type soundness theorem is always of the form “a well-typed program never does such and such”. It relates the static semantics (type checking) to the dynamic s

A type soundness theorem is always of the form “a well-typed program never does such and such”. It relates the static semantics (type checking) to the dynamic semantics (operational semantics) of a programming language. It doesn't make any sense to talk about soundness for dynamic languages, because there's no static semantics to relate to the dynamic semantics.