No, those are not equivalent at all. "Valid" means, intuitively, that if I skip the compile-time type checks, and run the program with the types checked at run

No, those are not equivalent at all. "Valid" means, intuitively, that if I skip the compile-time type checks, and run the program with the types checked at runtime. If the type system is sound, and the compile-time type checks all pass, then it is impossible to hit a runtime type error. More formally, a program is valid if the execution within the operational semantics (basically, the semantics of running the program) do not lead to an error. This is distinct from type checking correctly. Similarly, in formal logic "true" and "provable" are not equivalent. We'd like them to be, for sure, but the various incompleteness theorems ensure that we'll never be able to prove every possible true statement.