I would love to see an example of a proof for something like a text editor. How can people be expected to do this when the examples are always trivial toys, like array sorting? Show me a formal proof of something that in the trenches programmers can copy from. A proof of a basic todo list or something like that.
Why don't people use formal methods? (2019)
41–50 of 121 posts
Re: Why don't people use formal methods? (2019)
#42Earlier quoted context omitted.
Yep, I did submit bug reports. This was on Tuesday. I don't see a public copy of the mailing list that has my bug reports yet. The four bugs were: 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 f…
Very cool project and good finds. What do you see as the end state for your project - do you think pg has a path to upstream, or would this be a fork? 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.
Thank you for the kind words!
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.
Re: Why don't people use formal methods? (2019)
#43To me, "this returns sorted lists" illustrates the crux. 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 wha…
I was attending a conference back in, oh 2017 perhaps, where a few people from Microsoft were discussing their experience adopting TLA+ and somebody made the comment that they found that creating a spec was an exercise that could only meaningfully be done by the engineer (or perhaps team) writing the code. You wouldn’t, say, have an external TLA+ expert write the spec for you, but instead you would use the process of authoring the spec to ultimately learn more about your own design. And of course, perhaps avoid edge case bugs before they are written. Say what you want about Microsoft, but their observation does have a rather large sample size, and it sounded like formal methods was considered more impactful during software design rather than as software verification.
Re: Why don't people use formal methods? (2019)
#44I would love to see an example of a proof for something like a text editor. How can people be expected to do this when the examples are always trivial toys, like array sorting? Show me a formal proof of something that in the trenches programmers can copy from. A proof of a basic todo list or something like that.
That is always my problem too. I can see how to prove sort, if I was writing the standard library for my language I might do that (it is hard, but I hope whoever wrote my library did). However sort is already in my library. I'm writing code that does things much harder to write into a spec.
Re: Why don't people use formal methods? (2019)
#45Isn't the problem with formal methods that it isn't clear whether or not most of the useful code we use are actually formally verifiable? 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.
No, lots of problems can be expressed in a way that can be verified. But complete verification of an existing implementation is essentially impossible.
That doesn't mean that formal techniques are not useful, far from it. For example, AWS uses a formally specified model to verify if an implementation is correct by looking at the telemetry. See e.g.
https://p-org.github.io/P/advanced/pobserve/pobserve/
This isn't something you could meaningfully do with standard testing techniques, and it very compositional, you can do it piece by piece.
Re: Why don't people use formal methods? (2019)
#46I recently came across a use case where formal methods were incredibly helpful. I've been rewriting Postgres in Rust and am currently focusing on correctness. The biggest challenge is that there's so much surface area to cover. Postgres has over 3000 user-facing functions, ranging from regular expression matching to JSON iteration to computing the gamma function. About half of these functions are simple pure function…
> I've been able to formally verify that the Rust behavior is identical to the Postgres C behavior
I thought you wanted to get rid of the bugs!
Re: Why don't people use formal methods? (2019)
#47I think everyone knows the answer already - it's too hard to be worth it for most problems. The article doesn't disagree with that and was a good read anyway. Don't skip it because you already know the answer. 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…
I would say that most companies are just badly run, and blunder along stepping on mines periodically, making no effort to systematically manage risks. The uses for formal methods are often much bigger than verifying pure software components.
For example, the recent NTP outage at Telstra, a major telco, took their entire network offline, and major clients like railway systems were offline for days; the compensation will be massive. A fairly basic level of FMEA or robustness checking would have identified that (a) downsizing the people who maintained the NTP system expertise, (b) operating time as a SPOF, (c) running a telco as a retail chain, real estate investment portfolio, and marketing operation, with a subsidiary that does technology, results in fairly unbounded political and commercial liability.
Re: Why don't people use formal methods? (2019)
#48Earlier quoted context omitted.
> I found 4 different Postgres bugs. Bugs in the upstream Postgres C implementations? Did you report them or submit patches? I'm curious to see what you found!
Yep, I did submit bug reports. This was on Tuesday. I don't see a public copy of the mailing list that has my bug reports yet. The four bugs were: 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 f…
these are impressive findings, I am curious what was your process to convert existing code to formal verification languages like TLA+.
My basic understanding was to verify high level abstractions (e.g. transport ACK, fsyncs and so on), but verifying this deep probably requires complete verification of stdlib methods used by Postgres, otherwise how can you pinpoint culprit is the sscanf?
Re: Why don't people use formal methods? (2019)
#49I recently came across a use case where formal methods were incredibly helpful. I've been rewriting Postgres in Rust and am currently focusing on correctness. The biggest challenge is that there's so much surface area to cover. Postgres has over 3000 user-facing functions, ranging from regular expression matching to JSON iteration to computing the gamma function. About half of these functions are simple pure function…
> I've been able to formally verify that the Rust behavior is identical to the Postgres C behavior for over 1000 of them.
Since both Rust and C have LLVM IR intermediates, you could use KLEE[0] for this.
Re: Why don't people use formal methods? (2019)
#50We do. It's called a type checker. Every "formally verified" system is going to be partially verified. e.g. you might prove your sort procedure sorts, but did you prove its complexity? Under a cost model for integer compares or a cost model for page fetches? Or both? Multi-layer cache page fetch costs? How well you verify just depends on how well you decide to model the problem. Different type checkers have different…
One of my favorite quotes on this topic is: "Type systems are just the parts of formal verification we've figured out how to make fast."
given your experience on the topic, i'm curious: do you think that the reason we haven't figured out how to make other parts of formal verification fast is that, in general, programming languages expose each individual machine operation in the code, so the verification surface area is the combinatorial set over that? i've been working on a low level high opinion language, and its verifications are able to be checked in an extremely tight loop, largely because of the structure of the language itself.