Formal methods could be useful when requirements are clear, can be strictly defined, aren't going to change suddenly, and the stakes of building it wrong are very high. Avionics. Medical devices. Cars. Some kinds of embedded systems. Core parts of OS Kernels, databases, network stacks, cryptography libraries, etc.
Most software in the world is not like this. It exists to support businesses trying to make a buck in a changing world, either from consumers or from other businesses. Requirements are messy, shift frequently, and agreeing on what they are at all is more than half the battle. Nobody really knows the minutiae of quite how the whole product works but it doesn't really matter. Money is still coming in. The risk to those businesses of even rather bad bugs is generally low. A few customers have a bad day because they see a 500 error in their browser when they're trying to order food, or they can't summon their ride-share for 5 minutes. The issues are fixed and life goes on. The perfection of formal methods is the enemy of good, and would be a net negative return on investment, much as programmers who (understandably) love perfection and clarity and rigor might want it to be otherwise.
Some bugs can't be fixed: once you've leaked millions of people's personal information, you can't really take it back. The "stakes of building it wrong" are very high in most software, because businesses are all too willing to hoover up all your info.
> The risk to those businesses of even rather bad bugs is generally low.
That is unfortunately true, but hopefully we'll eventually manage to hold businesses accountable for their screwups.
We all make use of those components though, regardless of how CRUD the application is. We'd all benefit from them being validated. The fact that "fully validated" versions of those components don't exist is simultaneously an indication of how difficult the problem is and how little our industry truly cares about product reliability and quality. These issues are not rare or even particularly uncommon in the wild.
I imagine the pursuit of formal methods in software that doesn't strictly require it would go a long way to fixing other systemic issues like tech debt, security, and performance.
Not yet, but I think we’re getting to the point where software will fractionalize and those pieces will formalize.
TCP/IP stack, crypto libs, message busses, networking libraries are all prime candidates for this kind of formalization.
Right now we’re just waiting on the first mass incident where a component/service is recognized by a government as essential and should be regulated then you’ll quickly see those structures/organizations form around that area.
