While this is true, it's critical to note that "valid" here doesn't mean "valid as in it follows the intention of the programmer who wrote it" but instead "vali

While this is true, it's critical to note that "valid" here doesn't mean "valid as in it follows the intention of the programmer who wrote it" but instead "valid as in it either terminates in a well-defined error condition or completes to an identically-typed result" (preservation and progress). The engineering constraint is to ensure that the design and logic of the types themselves enable preservation-and-progress-validity to enforce meaningful semantic constraints. A sound and complete type system can still say things that aren't practically meaningful.