"It is not enough to return a string - you must return the correct string, and that is not normally not something a type can solve for you."

It can, however, ensure that you have returned a legally-formatted email address instead of someone's first name, with proper use of the type system. You'd probably be surprised what you can do with a real type system, based on what you're saying here. It is not a proof of correctness, but there's a great deal more possible than in Java.

It of course can not ensure you returned the correct email address, but often that's a much less pressing problem, because the thing returning the address may very well have had only one address in hand to chose from, in which case it can't be wrong. There's a lot of logic like that you can deploy in Haskell, when scopes and inputs to functions are much more carefully controlled than a traditional language.

Nowhere in his post did tikhonj suggest that compilation == correctness, even in Haskell. Of course it isn't. The only people making that assumption are wyqueshocec's coworkers, and naturally they're getting burned as a result.

The key point is that a sufficiently expressive type system gets you far closer to correctness on the basis of type checking alone than does a weaker static system like Java's or a dynamic one like JS's. You should still write tests, you just won't have to write as many in order to reach the same degree of confidence in your code.