My Haskell comment was regarding specification of the overall system, not tests specifically. It was a reference to the incredible type system.

> this "tests can prove correctness" idea

You are the only one putting forward such an idea. It's not that I think tests passing proves correctness. It's that I know from experience that I don't fully understand the system. The code that breaks is always a surprise to me because if it wasn't then I would have fixed it before it broke.

So if my code breaks and tests don't catch it then I figure that before I fix it I should add a test for it.

Of course there are some categories such as multithreading that you generally can't test. So you take extra care with those, and then inevitably end up sinking time into debugging them later regardless.