Comment by Animats
5 hours ago
I haven't seen the Lipton/Perlis/De Millo paper in years. I was around for that argument. Which really dates me. Those guys were pushing for mutation analysis.[1] 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.
It's taken way too long for verification to catch on. Here's where I was almost 50 years ago.[2] Part of the problem is that most of the interest came from people in love with the formalism. The notations used by most researchers were terrible, as is pointed out in the Lipton/Perlis/De Millo paper. You want a notation that matches the programming language.
We had the basic architecture back then - use a SAT solver on the easy stuff, and something with some AI capability on the hard stuff. We had the Oppen-Nelson simplifier, the first SAT solver, for the easy stuff. We had the Boyer-Moore prover for the hard stuff. It's Good Old Fashioned AI, and very good for the late 1970s. The SAT solver knocks off over 90% of the verification conditions. Then you want verification notation that creates hard but abstract problems for the AI solver. Like writing two asserts in a row, with the hard problem being to prove the second one from the first.
We didn't have enough compute back then. It took about 45 minutes on a VAX 11/780 for the Boyer-Moore prover to build up number theory from something similar to the Peano axioms. Now it takes about a second. I ported the Boyer-Moore prover to GNU Common LISP a few years ago, just to see it live again.[3]
With LLMs to do the grunt work, this is a lot less labor-intensive. And it's really needed to keep LLM garbage under control. Given a concrete goal against which to optimize, LLM coding is much more effective.
Formal specifications are still hard to write, but there are many important areas of software for which the specification is simple but an efficient implementation is hard. File systems. Databases. Networking. Some kinds of control systems. Stuff that really needs to work right.
[1] https://en.wikipedia.org/wiki/Mutation_testing
[2] https://www.animats.com/papers/verifier/verifiermanual.pdf
> 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.