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.
1) With formal verification you can prove properties about your system. With extensive testing you can also do the same but you need to take care and make sure you cover all possible cases.
2) With formal verification you can easily test things that are normally hard to cover by traditional testing. For example, if you want to test if that a postgres randomly goes offline, you don't lose any data, it's pretty hard to cover with extensive testing, whereas with formal verification you just say "postgres exists, it has state and can be online/offline, it can go online/offline at anytime" and you're covered.
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.
Facebook runs a number of quite complex internal distributed systems - databases, caches, proxies, etc. all of these are amenable to various forms of formal verification, and verifying them is the kind of thing that helps prevent outages and data loss.
Well. Facebook has invested a fortune in proving that its systems follow expected properties of respecting consent—that all the data flows that happen are permitted. That turns out to be helpful for them in avoiding fines.
Anything with a GUI seems really daunting to specify. And then later you need to update specs to match GUI if you make any changes and you need to decide which is wrong: the implementation of the specification.
Well, to prevent bugs in this layer, I guess? To not have things out-of-date or clickable when they shouldn't be or not have layout suddenly becoming garbled.
The final proof you get from formal methods is often irrelevant in my opinion. Most of the benefit comes from architecting the system so as much as possible can be verified and forcing yourself to make intentional decisions on the edge cases. The results are for other people.
I'm not sure you want to create a record of intentional decisions if you're at Facebook though.
> For some programs, the shortest descriptions of what they do are the programs themselves.
There is almost no real-world program for which this is true. One corollary of this would be that it is impossible to refactor the program to be any cleaner, which is not true for basically any large real-world program.
Another corollary of this is that no observable aspect of a program could be changed without breaking user expectations, but this too is almost always wrong (e.g. almost always, but not 100% via e.g. the famous xkcd comic about spacebar heating, a global performance optimization would be viewed as good).
I agree with this counterargument.
I mean, you can verify that Euclid's algorithm computes the GCD. Or that quicksort produces a sorted version of the input array.
But how do you verify Facebook? Facebook computes what?
For some programs, the shortest descriptions of what they do are the programs themselves.
Edit: I agree with the replies that you can verify individual parts and properties, like with testing.