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.

I found exactly the opposite to be true when I took formal verification at university, and that was the major point that made formal specification / verification unattractive to me.