[StilesCrisis]

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.

[eru]

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.

[akshayshah]

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.

[StilesCrisis]

Almost all software is internal "make the business run" software that we never see, or web pages. Very very few engineers would even consider making a new message queue. The crowd here is different than most :)