"The counterpoint is that specifications are closer to informal requirements than implementations are (and thus a mistake is easier to spot)."
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.
I think it very much depends on the domain. For instance, I've seen specs for floating point ops that were 1-3 pages compared to 30,000 lines of RTL. That holds pretty well for many other cases. For example, a properties like decompress(compress(x)) = x are beautifully simple compared to the details of the algorithms, and are pretty compelling correctness evidence.
Part of it may be that you need experience writing formal specifications just as you need experience writing programs; everyone has a lot of the second, but little of the first. They're related skills, but one does not carry over straightforwardly to the other. The first is a somewhat more abstract (but also much more concise and powerful) method of reasoning. This sort of skill hasn't been taught well in CS education yet, owing to the fact that the underlying tools were too niche.
Everyone knows that the weak link is the specification. But this is a spurious argument, since, by definition, if you guarantee the implementation the only thing that's left exposed is the spec itself. At least you're reducing the attack surface
I haven't seen the Lipton/Perlis/De Millo paper in years. I was around for that argument. Which really dates me. Those guys were pushing for mutation analysis.[1] That's a test for the test suite - you make some random change to the program and see if the test suite catches it. Fuzzing is related to that concept.
It's taken way too long for verification to catch on. Here's where I was almost 50 years ago.[2] Part of the problem is that most of the interest came from people in love with the formalism. The notations used by most researchers were terrible, as is pointed out in the Lipton/Perlis/De Millo paper. You want a notation that matches the programming language.
We had the basic architecture back then - use a SAT solver on the easy stuff, and something with some AI capability on the hard stuff. We had the Oppen-Nelson simplifier, the first SAT solver, for the easy stuff. We had the Boyer-Moore prover for the hard stuff. It's Good Old Fashioned AI, and very good for the late 1970s. The SAT solver knocks off over 90% of the verification conditions. Then you want verification notation that creates hard but abstract problems for the AI solver. Like writing two asserts in a row, with the hard problem being to prove the second one from the first.
We didn't have enough compute back then. It took about 45 minutes on a VAX 11/780 for the Boyer-Moore prover to build up number theory from something similar to the Peano axioms. Now it takes about a second. I ported the Boyer-Moore prover to GNU Common LISP a few years ago, just to see it live again.[3]
With LLMs to do the grunt work, this is a lot less labor-intensive. And it's really needed to keep LLM garbage under control. Given a concrete goal against which to optimize, LLM coding is much more effective.
Formal specifications are still hard to write, but there are many important areas of software for which the specification is simple but an efficient implementation is hard. File systems. Databases. Networking. Some kinds of control systems. Stuff that really needs to work right.
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.
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.
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.
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).
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.
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.
It's taken way too long for verification to catch on. Here's where I was almost 50 years ago.[2] Part of the problem is that most of the interest came from people in love with the formalism. The notations used by most researchers were terrible, as is pointed out in the Lipton/Perlis/De Millo paper. You want a notation that matches the programming language.
We had the basic architecture back then - use a SAT solver on the easy stuff, and something with some AI capability on the hard stuff. We had the Oppen-Nelson simplifier, the first SAT solver, for the easy stuff. We had the Boyer-Moore prover for the hard stuff. It's Good Old Fashioned AI, and very good for the late 1970s. The SAT solver knocks off over 90% of the verification conditions. Then you want verification notation that creates hard but abstract problems for the AI solver. Like writing two asserts in a row, with the hard problem being to prove the second one from the first.
We didn't have enough compute back then. It took about 45 minutes on a VAX 11/780 for the Boyer-Moore prover to build up number theory from something similar to the Peano axioms. Now it takes about a second. I ported the Boyer-Moore prover to GNU Common LISP a few years ago, just to see it live again.[3]
With LLMs to do the grunt work, this is a lot less labor-intensive. And it's really needed to keep LLM garbage under control. Given a concrete goal against which to optimize, LLM coding is much more effective.
Formal specifications are still hard to write, but there are many important areas of software for which the specification is simple but an efficient implementation is hard. File systems. Databases. Networking. Some kinds of control systems. Stuff that really needs to work right.
[1] https://en.wikipedia.org/wiki/Mutation_testing
[2] https://www.animats.com/papers/verifier/verifiermanual.pdf
[3] https://github.com/John-Nagle/nqthm
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.
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.
I'm not sure you want to create a record of intentional decisions if you're at Facebook though.
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).