I thought this article from Jane Street makes a nice complimentary pairing.

In a good 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 the 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 blue print.

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.

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.

Of the 3000 functions, I've been able to formally verify that the Rust behavior is identical to the Postgres C behavior for over 1000 of them. In the process, I found 4 different Postgres bugs. All of them would not be triggered under ordinary usage, but one, if triggered, would corrupt your database.

I think why formal methods works well for this is I'm testing a large number of small to medium self-contained pieces of code. For each of them the specification is simple: does postgres_fn(args) == pgrust_fn(args). I've been using Kani[0] which works across both Rust and C code so the proofs are based off the actual code and not a translation of the code to another language.

If you want to check out what all the verification look like, you can see them here[1]

[0] https://github.com/model-checking/kani

[1] https://github.com/malisper/pgrust/tree/main/proofs

The article mentions NP-complete, but is it actually a solvable problem in general?

> For extremely restricted cases, like propositional logic or HM type-checking, it’s “only” NP-complete.

Maybe this is like Quaternions, that are actually very easy and useful, but suffer from confusing descriptions. Or maybe more like Monads, which are actually very abstract, and may not be suitable unless your the sort who understands Mathematician style mathematics.

More to the point: I'm not even sure how I would get started and evaluate them tacitly.

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.