>Tests not failing when your code does implies that you are missing test cases. In other words things are underspecified.

I am really confused. Have you guys never written any multithreaded code? You can write the most disgusting thread-unsafe code without a single lock and be perfectly green on all your tests. And who in the world can write tests to simulate all possible timing scenarios to test for race conditions?

I give multithreading as just the most egregiously obvious example that this "tests can prove correctness" idea is fundamentally broken, but I think it applies more generally.

>Haskell is the extreme example of this. If it successfully compiles then it most likely does exactly what you intended but it might be difficult to get it to compile in the first place.

Absolutely 100% of the safety of haskell comes from the mental model (functional programming, immutable data structures etc) and none from the test cases (although their community appears to even do testing slightly better than others).