> What would it mean for code to be semantically correct while containing type errors? It would probably mean that the code is not in fact semantically correct

> What would it mean for code to be semantically correct while containing type errors? It would probably mean that the code is not in fact semantically correct because some semantic edge cases are not covered by the tests. It can also mean that the code has incorrect subprograms, but that the program as a whole is protected from them by some hard to analyze condition. As an extreme example, one of these two programs "works": if goldbachConjectureCounterexampleExists() then print("Hello world!") else launchMissiles() if goldbachConjectureCounterexampleDoesNotExist() then print("Hello world!") else launchMissiles() but I don't know which and neither does the compiler. Rejecting them is a feature, not a bug.