Comment by gr_norm
6 hours ago
Agree in part, but remember that formal verification need not be done in full. By analogy, we don't avoid testing simply because everything under the sun can't be tested. Even simple things like verifying that certain API endpoints are idempotent, or as a few steps up, that the datastores used by Facebook have distributed consistency and fault-tolerance properties, are of enormous utility.
Exactly, it feels dishonest that this point is so rarely brought up in essays on formal methods. You can do things like prove that all possible faults are always caught, or any memory that is accessed has first been malloc’d, or that the API endpoint will always respond (liveness). These are often both easy to specify and difficult to guarantee with conventional testing.
I’m a bit confused as to what makes formal verification different from extensive testing.
To a first approximation, formal verification can guarantee some property holds for every possible run of the program, rather than just the tested ones. It's a lot more powerful than it sounds, because this unlocks the ability to talk about qualities of programs that cannot be tested (effectively or at all). Hyperproperties like confidentiality, integrity, and availability tend to be quite difficult to test, for instance.