The title may be slightly misleading if you haven't bothered to read the article. It's responding to a famous paper from 1979 critiquing formal verification. The article ends up disagreeing with most of its strongest claims in hindsight, though a couple appear to remain worthwhile.

> Real-world systems are too messy to be specified

I agree with this counterargument.

I mean, you can verify that Euclid's argument 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.