This moving of goal posts whenever correctness through type systems is being discussed is a bit tiresome, because it quickly leads to such ad absurdum corner cases.

Yes, you are all correct. The compiler may have a bug. And if it does not, then the type system may have a problem. And if it is formally verified, then the theorem prover might have issues. And if it does not, then the very math it relies on may be wrong.

But what do we contrast this to, what is the alternative to correctness through the type system? Almost every time, when it isn't "nothing", it's "tests". We rely on tests to test whether the program behaves correctly.

And as we all know, quite in contrast to type systems and their checkers, tests are always error-free, complete, and sensible?