So, I read your story more carefully. I will have to apologize to my knee jerk reaction. You don’t paint a false dichotomy directly, but the comparison itself suggest there is some opposition between the two. i.e. “Shocking secret about types is they don’t find all the bugs, and testing can’t be avoided!” If the title was “You should test your code whether it’s well typed or not!”, I think it may not have gotten my attention and I may have not succumbed to my own confirmation bias and written it off as “yet another types vs tests… diatribe”
BTW under some circumstances type-correctness does guarantee program correctness where program correctness is narrowly defined as “it does implement the specification” correctly. These circumstances are mostly academic and in the real world, I’ll have to agree with you. I also will have to say TDD is great because it requires you to think about “what does it mean for my code to be correct” up front. You write down your expectations as tests, but in some rare circumstances you can write down these specifications better in types. The good thing about tests and types, is computer can run or check them letting the computer do the job of finding all your mistakes!
It’s amazing that a good deal about getting a programing problem right devolves into “think real hard up front”. Types AND tests are both great mechanisms for doing that thinking. We all should be praising them and not putting them in conflict.