> It's sound (Rejects all incorrect programs), decidable (There is an algorithm to reject all incorrect programs) but due to Godel's decidability problem they're incomplete (There are always correct programs which the type checker rejects as incorrect).
Isn't that the definition of "semidecidable" as distinct from "decidable"? A decidable question is one where you can determine the answer, whatever that answer may be. A semidecidable question is one where, if the answer is yes, you can determine that, and if the answer is no, you may not be able to determine that.
If you can always show that a program is incorrect, but you can't necessarily show that a program is correct, then the correctness of a program isn't decidable.
Isn't that the definition of "semidecidable" as distinct from "decidable"? A decidable question is one where you can determine the answer, whatever that answer may be. A semidecidable question is one where, if the answer is yes, you can determine that, and if the answer is no, you may not be able to determine that.
If you can always show that a program is incorrect, but you can't necessarily show that a program is correct, then the correctness of a program isn't decidable.