Join the discussion
Write your take first — we'll ask for email only when you're ready to publish.
- Hacker News
- Pretty much every job I've had has involved integrating with highly imperfect, changeable, and inaccurately implemented (and barely documented) third party APIs. That's where most of the work went and I don't see formal methods improving the situation any time soon.by dcminter
- Because 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.
by StilesCrisis - 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.
by akshayshah - The ironic thing is that LLMs are what will make formal methods feasible.
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.
by eru - I've been a big nerd for formal methods for quite awhile, and have been broadly unsuccessful in getting employers onboard.
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.
by tombert - Software engineers are rarely engineers at all, and pretty much never know anything about computer science.by epolanski
- > 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
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.
- > designing stuff with TLA+, then feeding the spec into Claude
That seems to defeat the purpose of using TLA+ in the first place. It's taking a rigorously logical and proven specification, putting it through a black box (that you don't own and cannot inspect) with indeterminate and unknown process, to get executable code that may or may not have anything to do with the specs.
Unless you feed the code back into something to verify that it corresponds with the specs? Is there nothing that can turn the specs into executable code directly and deterministically? Why involve a language model at all?
by lioeters - This blog is actually very useful... There's also the flip side, possibly due to the expense (technically, intellectually, and emotionally), where "IT'S FORMALLY VERIFIED!!" has become some marketing code for "it's safe, secure, and PFAS free..." - just because something is formally verified, doesn't mean it's secure or fit for purpose. It usually just means it conforms to a given spec "and that's that..."by unprovable
- 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.by taybin
- 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.by warkdarrior
- > A proof of a basic todo list or something like that.
Just using a verb here would be a first step toward rigorous thinking. A proof that a todo list does what?
by mrkeen - 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.by bluGill
- I believe I proposed that somewhere because it was a small, useful app which often opened malicious payloads. People may or may not fully prove it.
What I thought would be useful is, like Ironsides DNS, a SPARK Ada or other implementation that shows no code injections could ever happen from loading, modifying, or rendering text. That's a useful subset of full verification.
If not that verified, writing things in a memory-safe, concurrecy-safe language covers lots of ground. Rust and Pony put good effort in those areas. In Rust, I think you still had to manually turn on checks for some overflows which hurt performance a lot. So, static analyzers or automated provers for range properties have a performance benefit.
Muen is the largest, production project I know in such a language:
Ironsides was an earlier project:
- https://blog.janestreet.com/formal-methods-at-jane-street-in...
I thought this article from Jane Street makes a nice complimentary pairing.
by s_dev - And it’s not just blogs. They’ve got an open job posting [0] for a ‘Formal Methods Engineer’.
[0] - https://www.janestreet.com/join-jane-street/position/8585303...
- And this pairs nicely with Jane Street's observation that agentic coding changes the formal proof equation: https://news.ycombinator.com/item?id=49064854
Formal proofs of code are almost beyond the capabilities of the best human programmers (3.7 lines per day!), but LLMs can bash out code at an amazing pace. It's often crap, sadly, but the proof they are bashing out is the hard bit. If possible at all, the task is EXPTIME. Verifying the proof is only P, so when it's wrong you tell the LLM to do it again. A stable agentic loop is what makes it possible. The results in the article I linked to speak for themselves.
by rstuart4133 - I think it's the culture is software engineering.
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.
by asxndu - I enjoyed this quote from the article, which concisely summarizes the first part of the above comment:
> “website isn’t airplane!!!”
by antonvs - Also you can write a perfect specification get into implementation and have to step back and redesign.
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.
by kalcode - I 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 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.
by IshKebab - Formal verification is also extremely common in the software design world, to be fair. Most programming languages in use have at least a primitive type system and even those that historically didn't are gaining them (e.g. Typescript, Python gradual typing, etc.)
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.
by win311fwg - 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.
by angry_octet - In most industries that need software made for them it's hard enough to get people to care about spending enough time on informal methods let alone formal ones. I simply don't think most of the industry has had the breathing room and respect for engineering for this pattern to develop.by SCdF
- I think its also about tolerance for failure. For software that must not fail or where reliability commands a premium you would be wise to invest in formal methods. Core systems at aws for example. For throwaway CRUD code its just easier to try iterations on the problem and call it a day. Its not about respect just RoI.
- I think programmers in general do not give much thought to the level of engineering required for a task.
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.
by forinti - We 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 modeling features.
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.
by ndriscoll - I think there's an element of this which really breaks down to the type system being the part of formal verification that we've figured out how to do during the course of implementation.
Software engineers (myself included, over the years) often argue their real value isn't just writing code, its figuring out the gaps in requirements and how to resolve them. Sometimes that engineering process gets turned back into a formal spec. But much more often, the implementation functionally becomes the spec and contains many details that were never present in the original statement of the requirements.
Formal verification techniques in general are a harder sell until we get the industry to a point where there's broader agreement that what we call "implementation" is often a blurry mix of spec development, prototyping, and actual implementation all happening at the same time.
by sethhochberg - 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."
by yoshuaw - To 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 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.)
by teiferer