Certain teams do suffer from incorrectness they produce, and I think obsession with correctness can be beneficial for them. But it's a painkiller, not a cure.

Certain teams do suffer from incorrectness they produce, and I think obsession with correctness can be beneficial for them. But it's a painkiller, not a cure. Once you build a good team, the source of incorrectness shifts to the vagueness of the requirements and domain complexity. And indeed, attempting to solve it (be it with types or with tests) is pointless. In essence, if your team finds a lot of benefits in types, you have a mediocre team. And mediocrity is almost unavoidable at scale, that's why big companies heavily invest into those correctness procedures (unit tests, types, various forms of bureaucracy, etc).