As someone who uses strongly, statically typed functional languages (dependent ones like Coq no less), and who rarely writes unit tests, I downvoted you because

As someone who uses strongly, statically typed functional languages (dependent ones like Coq no less), and who rarely writes unit tests, I downvoted you because you're wrong. Specifically: > the type system of the program proves the program correct. Is not a valid statement, unless you're actually writing proofs in Coq. I bet you aren't. "The type system of the program proves many simple properties of the program correct" is much more correct. Also: > Because my code has no mutable state No, that's not why. The type system you use may be incapable of reasoning about mutable state, which coincidentally serves to indicate that it most likely can't reason about such things as "this list is sorted", further supporting my initial counterpoint. Check out ATS or Why for examples of languages that permit reasoning about mutable state.