Why Don't People Use Formal Methods? (2019)(hillelwayne.com) |
Why Don't People Use Formal Methods? (2019)(hillelwayne.com) |
Of the 3000 functions, I've been able to formally verify that the Rust behavior is identical to the Postgres C behavior for over 1000 of them. In the process, I found 4 different Postgres bugs. All of them would not be triggered under ordinary usage, but one, if triggered, would corrupt your database.
I think why formal methods works well for this is I'm testing a large number of small to medium self-contained pieces of code. For each of them the specification is simple: does postgres_fn(args) == pgrust_fn(args). I've been using Kani[0] which works across both Rust and C code so the proofs are based off the actual code and not a translation of the code to another language.
If you want to check out what all the verification look like, you can see them here[1]
Bugs in the upstream Postgres C implementations? Did you report them or submit patches? I'm curious to see what you found!
0) When parsing a macaddr[0], Postgres uses sscanf with %x. %x can wraparound. This means SELECT '10000000aa:bb:cc:dd:ee:ff'::macaddr; will return aa:bb:cc:dd:ee:ff.
1) When parsing a tid[1], Postgres uses strtoul. The return value of strtoul is different across platform for the empty string. This means on some platforms Postgres SELECT '(,5)'::tid; will error and others will accept it.
2) Postgres missed an overflow check in it's cash type[2]. When running SELECT '-92233720368547758.08'::money / (-1)::int8; some platforms will error and other's will return the MIN value. Postgres does check for this for some of the other cash related functions, but it missed it for one of them.
3) When hashing the "char" type Postgres will cast a char to an integer[3]. On some platforms char is signed and on others it's unsigned. This means the hash of a char can be different depending on the platform. If you are using a hash index or hash partitioning on a char and move your DB from x86 to arm, the hashes will differ and your index/partitioned tables become corrupted. Note that this is special char type that you have to refer to by "char" that is separate from the typically used CHAR(n) type which is what you typically use, hence this would never come up under real usage.
The common pattern with all of these is they rely on C behavior that differs across platform (integer overflow, char signedness, strtoul). Rust is better about having more consistent behavior across platforms so these cases get flagged when the Rust code and the C code differ.
[0] https://github.com/postgres/postgres/blob/REL_18_3/src/backe...
[1] https://github.com/postgres/postgres/blob/REL_18_3/src/backe...
[2] https://github.com/postgres/postgres/blob/REL_18_3/src/backe...
[3] https://github.com/postgres/postgres/blob/REL_18_3/src/backe...
You may know exactly what you want, and you may have a reasonably fast and cheap way to verify your code against a formal specification. But the formal specification needs to come from somewhere and for any non-trivial program its complexity is going to be in the same order of magnitude as the code implementing it. So we are back to writing "code" (which is what a formal specification is) that needs to be checked against what we actually want. And that "code" needs .. a test? Hard thinking? A formal verification itself?
Don't believe me that this is hard? Back to "this returns sorted lists". The promise of formal verification is that whatever implementation I throw at the verifier, as long as it passes the check, I'm happy (assuming that I can also encode things like running time and resource use). Now imagine a program that always returns the empty list. It satisfies "this returns sorted lists" trivially but is not at all what we want. The formal spec has a bug. Such issues can be subtle in larger projects and no amount of model checking or SMT solvers can guard you against a bug in that "code".
Don't get me wrong, it can be incredibly useful. But it's not the silver bullet that some proponents make it out to be. It's another tool next to testing, not instead of it. (The whole "testing can only prove the existence of bugs, not their absence, that's why we should use formal verification instead" is just misguided at best and propaganda at worst.)
This is a more useful perspective; it's not "we do/don't use formal methods," but instead "how can I more precisely model my domain?" Helpfully, if you model your domain well, code tends to be obvious/write itself.
"Type systems are just the parts of formal verification we've figured out how to make fast."
Still, it's a long journey, and academic formal verification would always be, by design, a few steps ahead of what the industry can do efficiently in practice.
Mostly, there's too little, but there are many cases when there's too much. I see people writing tons of tests for corporate software that will be used by a couple of people and will have to be updated regularly anyway.
Building a hut is not the same as building a skyscraper, but we don't really have guidelines for different software projects. No methodology I've ever seen distinguishes types of projects by complexity.
I thought this article from Jane Street makes a nice complimentary pairing.
I have pretty cynical opinions as to the "why" of this, largely involving the fact that the vast majority of software engineers refuse to learn anything that they weren't explicitly taught in college, but regardless of the reason whenever I have tried proposing TLA+ in the past, people will nod along and wait for me to stop talking. I've had several managers say "they'll look into it", which was such an obvious lie that I don't know why they even bothered.
I've "snuck in" TLA+ usage a few times. I gave up on getting anyone else to use TLA+, but as I've gotten more senior-level, I have been given a fair bit more leeway on how I approach projects and as such I have been able to budget myself a day or two to model some of the less-obvious bits of concurrency.
All that said, I have had some luck with designing stuff with TLA+, then feeding the spec into Claude and getting that to implement the actual executable code. Maybe I'll be able to convince an employer that's a good use of time now.
I think it's not only SWEs, but general persons that goe to college primarily to get a job, without having a natural curiosity for things.
Maybe this is like Quaternions, that are actually very easy and useful, but suffer from confusing descriptions. Or maybe more like Monads, which are actually very abstract, and may not be suitable unless your the sort who understands Mathematician style mathematics.
More to the point: I'm not even sure how I would get started and evaluate them tacitly.
Of particular confusion: Does formal verification lead to a strange-loop style or "It's verification all the way down" scenario, where you are shifting the correctness from the original code to the verification? Then must verify the verification ad-infinitum? (This is almost certainly wrong, but I don't grasp why)
The big question I ask: "Would I rather have a code base with formal verification, or one in which all the time and effort used by add that were spent using and testing the software in a practical way; or code reviewing it"
In a food delivery app/social network it seems like a waste of time to use formal methods.
When designing software for aircraft, pacemakers, fintechs, cryptography and DeFi protocols there is a bit of value for formal methods. The problem is that often, people with the food app/social network culture are hired to build DeFi protocols.
Which explains why so much money is being stolen form DeFi protocols of late. So why people don't use formal methods.
- 95% of the time, the stakes are low
- 5% of the time, the engineers don't understand the value of formal methods.
Leslie Lamport once joked that if software developers were architects, they would first build a skyscraper and then later draw the blueprint.
Software is fast to iterate and test that a lot assumptions can be proven by actually writing the code.
Software is closer to gardening or painting. We discover a lot through practice and writing code. Then we can often write more formal specifications.
But formal method is impractical for most software upfront, and instead is likely used for more serious runtime failures or cost of life.
That's just my two cents.
> “website isn’t airplane!!!”
The article mentions NP-complete, but is it actually a solvable problem in general?
> For extremely restricted cases, like propositional logic or HM type-checking, it’s “only” NP-complete.
Most programs don't need to be rigorously perfect. If they did, LLMs wouldn't be as popular as they are right now.
If you're dealing with medical equipment or space flight, maybe there's a need. But usually the goal is to make errors _inexpensive_ to find and fix, not theoretically impossible.
First: LLMs find so many bugs and security holes in software right now. So you pretty much have to prove your stuff correct, if you don't want to get hacked into.
Second: LLMs make it much easier to apply formal methods. Just ask Claude to prove your stuff in Lean or whatever, no PhD required anymore.
IMO the reason is way more on the "it's too hard" side than "it isn't worth the effort". Formal verification is extremely common in the silicon hardware design world, despite its extreme cost (the tool licenses cost on the order of $100k per seat, as far as I can tell). And in this domain bugs are really expensive. But I think it would be used in spite of that simply because it is an order of magnitude easier than software formal verification.
I don't know if there is any solution to that. Software itself is an order of magnitude (or more) more complex than hardware... I think the author's suggestion of partial verification is the way to you. You're not going to formally verify your GUI but you could formally verify your LZ4 decoder. Maybe.
The question is, as always, to what degree do the returns start to diminish. The Rust crowd laughs at Go's level of formal verification and says that their level of formal verification is the right level, but then the Lean crowd laughs at Rust's level of verification and says that their level of formal verification is the right level. The universe laughs at all of them. For crowds so concerned about mathematical proofs, it is funny that they end up right back at gut feeling.
This is deeply related to the conceptual error a lot of executives are currently making around automation in/of their software engineering orgs.
It has always been true that learning some formal methods probably makes you a better programmer in certain ways, even if you never use them. I think it's increasingly also true that learning some formal methods probably makes you a better manager of people/processes that product software.
The key skill - which is rare - is knowing exactly how much analysis to do.
Formal methods are appealing because they suggest that full analysis is possible. But formally proved programs can still have bugs!
That said, your broader point is more or less correct. I think the advantage of something like TLA+ is that the specs can generally be more abstract and as such the checks can be more exhaustive than you would likely get with regular "code".
With concurrent code, in particular, it can be difficult to know if your algorithm is correct, especially without the confounding variables that you get with a "real" programming language. Is my program broken because of some memory allocation quirk? Is it broken because of some peculiarity with how pthreads are dispatched? Or is my design wrong? Being able to work at an abstract level at least can check the last part.
Of course, though, you are correct that formal methods aren't silver bullets.
And of course, that raises the issue of what do you want to do about ties....
The promise of formal verification (and testing) is essentially the same promise as double-entry accounting. It assumes that if you do the same thing twice that it is unlikely you will screw it up in the exact same way twice. When there is disagreement it tells you that something went wrong, but you still need to look at both sides to determine which one is wrong. There is no such thing as a panacea, of course.
> It's another tool next to testing, not instead of it.
Theoretically it is instead of. They both are trying to solve the exact same problem. The real world with real constraints isn't so neat and tidy, so they don't end up perfectly overlapping.
Without knowing anything about the pg team, I would assume they would be hesitant to even consider an under the hood switch, just from a risk management perspective, regardless of test coverage and formal verification. But I could be wrong.
My goal is to build the best database possible. I'm trying to imagine what Postgres would be like if it were built today. I've been able to make a bunch of big architectural changes that the Postgres team has been talking about but hasn't yet made. For example, threads instead of processes and a vectorized executor.
I think everyone would agree the types of changes I'm making are good ones. The challenge Postgres faces is there's millions and millions of Postgres databases out there so they are focused on minimizing the risk of breaking any existing functionality over doing a big high risk rearchitecture.
I could see ideas from what I'm doing gradually making their way into Postgres, but I think the odds that pgrust (or any Rust code for that matter) gets merged into Postgres is close to zero.