> I don't see how static typing helps with "solving the wrong problem" kind of issues at all. One example is F#'s unit of measure system, which can statically

> I don't see how static typing helps with "solving the wrong problem" kind of issues at all. One example is F#'s unit of measure system, which can statically verify dimensional agreement of arithmetic. Another example would be differentiating between "Safe Strings" and "Unsafe Strings" (say, untrusted user input) and statically enforcing which are allowed in which method. They won't tell you that "Facebook for Dogs" is a bad idea, but they may reveal subject-matter errors in the actual requirements themselves. Most test suites wouldn't even catch these errors, because test assertions are generally based on requirements. You could write your own unit-verifier that you run in tests, but then you're just reinventing static typing. In fact it's a common criticism of test suites in dynamically typed languages that they end up poorly reinventing checkers for the guarantees already provided by a decent static type checker. > I noticed here that you didn't make any difference between testing, PBT, MT and proof systems I also didn't differentiate between the Late Middle Ages and the Early Renaissance, because it was off topic. But if you insist: "Property-Based Testing" is a testing pattern, not a different kind of test. Write tests and assertions as appropriate for the thing you're testing. It seems to me that you should have enough understanding of the likely failure scenarios and edge cases of your code that you don't need to be randomly generating inputs, but I can see how it'd be useful. I test all sorts of invariants in my tests. This just doesn't seem like a novel thing to me. "Mutation Testing" is basically testing your testing methodology. Okay. You could also test your bus factor by randomly shutting out one developer for a day each month and seeing how you get on. Maybe good ideas for some companies? If you find yourself trying to develop a completely airtight testing process that will catch 100% of bugs, it's probably because too many bugs are passing your tests. Before you kill yourselves trying to develop an airtight, mathematically-guaranteed strong test system, may I suggest strong static type systems instead? Just let the compiler do it. "Proof systems" are strong static type systems.