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.

▲

angry_octet 2 hours ago | parent | next [-]

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.

▲

win311fwg 3 hours ago | parent | prev [-]

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.

▲

IshKebab an hour ago | parent [-]

It's a continuum... but I would say even Rust's type system is not in the realms of "formal verification". I think you need at least some kind of refinement types so you can say "an integer between 1 and 10" before you can stake even a vague claim to "formal verification".

So I don't think you can say it's common in the software world.

	▲	win311fwg 34 minutes ago \| parent [-]
		Specifying that a value must be an integer between 1 and 10 is most certainly further down the continuum than only specifying that a value must be an integer, but both define a theorem about the program that can be validated. How is the latter not formal verification? It's the same thing, only differing by degree.