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.

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.

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.

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.

> But how do you verify Facebook? Facebook computes what?

You start by verifying the permissions structure for Facebook posts.

And by verifying the shortest, least complex functions in Facebook's server side code base.

> 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).

Yes. No Silver Bullet (1986) said that 40 years ago.