Has anyone been experimenting with AI and formal methods - verification, proofs, or anything else? I've been thinking about this space quite a bit lately. For sufficiently interesting AI generated software, AI is also incapable of reviewing it - possibly for the same reason that humans are. AI ought to be able to adopt the formal methods humans have used to work around the inability to verify something just by looking at it hard. If the cost of adoption is what stopped us, thats no longer an issue.
Why don't people use formal methods? (2019)
51–60 of 121 posts
Re: Why don't people use formal methods? (2019)
#52My 2c I don't understand any of the material I've read describing them. What I do understand makes them sound like it will be a load of work for questionable benefits. If I end up writing safety-critical code. (Aerospace firmware, big robots etc), I will get over this hump and learn them. If not, I am not yet compelled; rather intimidated. Maybe this is like Quaternions, that are actually very easy and useful, but su…
> 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?
IANA formal methods guy, but my understanding is: yes, you're shifting the correctness burden from the code to the spec.
So why is that better? Because the spec is much shorter and more focused -- it strips out all of the implementation details.
It's bad to say "you have to trust this 100,000 line program." It's much better to say "you have to trust this 100 line spec, and the code that verifies it."
Re: Why don't people use formal methods? (2019)
#53Earlier quoted context omitted.
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 on…
For other interested spectators, I found this post by the author to be a good example of architectural changes in pgrust (along with motivations): https://malisper.me/the-four-horsemen-behind-thousands-of-po...
Re: Why don't people use formal methods? (2019)
#54My 2c I don't understand any of the material I've read describing them. What I do understand makes them sound like it will be a load of work for questionable benefits. If I end up writing safety-critical code. (Aerospace firmware, big robots etc), I will get over this hump and learn them. If not, I am not yet compelled; rather intimidated. Maybe this is like Quaternions, that are actually very easy and useful, but su…
> 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? IANA formal methods guy, but my understanding is: yes, you're shifting the correctness burden from the code to the spec. So why is that better? Because the spec is much shorter and mo…
That is a great explanation!
Re: Why don't people use formal methods? (2019)
#55Earlier quoted context omitted.
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."
Thankfully this is no longer strictly true. So, I think the quote needs a slight adjustment, "Type systems and $THING are just ...", but $THING is not very well defined yet. Between "linters", and other relatively fast AST-based rule enforcers, some of which looking at higher order behavior, I think we now have an amalgamation of formally verified concepts that we can consider fast enough and sufficient exercised in…
The field really needs more popularizers. I mean people or projects who can do "advertising" like, "if you add our linter to your CI/CD pipeline, you'll never have X class of bug ever again!"
Re: Why don't people use formal methods? (2019)
#56Because there is almost never a business need? 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.
I'm not sure how to think about what you mean by "almost never." If most commercial software is web frontend + monolithic app code + relational DB, then you may very well be right.
That doesn't quite match my professional experience, though - there are so many companies building databases, message queues, filesystems, and similar infrastructure. Sometimes they're internal projects, and sometimes they're commercial products. I've always felt that those systems would benefit from formal methods, since they're usually trying to provide strong guarantees to the application code on top.
Re: Why don't people use formal methods? (2019)
#57When I interviewed at AWS, I asked this question directly to their formal methods expert. Her response was two-fold:
1. All our code changes too much, we wouldn't be able to formalize it before it needed to change.
2. We already did this where we could, you just don't see it.
I didn't get the job and remain very skeptical on both answers. I think they just didn't have enough power internally to change the move fast and break everything culture for the better.
Re: Why don't people use formal methods? (2019)
#58I 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…
This guy is the real thing.
Re: Why don't people use formal methods? (2019)
#59To 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've been using TLA with claude code at work and it roughly takes twice as long, but it's already _fast_ to get claude to produce code and this prevents a lot of rework.
Re: Why don't people use formal methods? (2019)
#60I 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.
My guess is that the formal spec for a basic TODO list app is the same size as the source code of the app itself.