Comment by pfdietz
4 hours ago
> We didn't have enough compute back then.
The problem here is that more compute also helps testing. So it's not clear verification will pull ahead over just doing more testing, especially if there's any manual part of the verification workflow. The bugs that remain after testing become more and more difficult to stimulate.
> That's a test for the test suite - you make some random change to the program and see if the test suite catches it. Fuzzing is related to that concept.
Mutation testing is kind of orthogonal to random input testing or fuzzing. In fact, one can use the latter to automatically kill mutants in the former, which is very useful in automatically constructing enhanced test suites. You still need to determine what the correct behavior is for each new test input.
> The problem here is that more compute also helps testing.
A useful practical way to look at formal methods is "just" as testing on steroids, rather than as competition for testing. The pros and cons are mostly the same: Depending very much on their skill level, the practitioner gets a definite but finite improvement in correctness and particularly resistance to regressions, for the cost of additional upfront time and ongoing friction during maintenance. The main difference is the amount of "punch" in each passing spec requirement, which can be equivalent to an infinite number of concrete passing tests. (In the other direction: Ordinary testing using a few handpicked example (input, expected output) pairs is formal verification, just of an especially thin kind.)
Sitting in between ordinary manual tests and formal verification of entire program properties is property-based testing like Haskell Quickcheck, which offer some of the benefits of both.