just remember blueprints can also be wrong

Yeah, it's extremely important to note that any correctness technique - tests, types, contracts, formal methods - only provides _more_ confidence, not _complete_ confidence. We have to think of defense-in-depth.

Cool and impossible to apply to real world projects due to budget or deadlines.

There is an [interesting paper](http://lamport.azurewebsites.net/tla/formal-methods-amazon.p...) about how they use TLA+ at AWS to find bugs in their algorithms, and eventually prove correctness. So if you use AWS and rely upon its correctness, you have indirectly used a real-world application of TLA+. Someone else mentioned Facebook here, I think they also use formal methods.

Sure, formal methods are irrelevant for your standard CRUD application. However, the use case of AWS got me interested in applying TLA+ to this real-time collaboration feature that we have in the application that I develop. It involves multiple clients communicating over WebSockets, locking and unlocking resources, etc... Expressing the algorithm to TLA+ has:

1. vastly improved my understanding of what is going on and what the potential bad scenarios are. Simply taking a step away from the code, model the high-level algorithm and writing down the invariants that should always hold, makes a big difference.

2. identified real bugs that can occur (and probably have).

So yeah, you can't apply formal methods for everything. But I was pleasantly surprised by how easy it is to express a distributed algorithm in TLA+ and start proving statements about it. Somehow TLA+ manages to bridge the gap between engineering and more theoretical computer science.

Absolutely true. There is no way that a web tech company like Facebook could apply formal methods in such a fast moving world. Also, don't click this link, it doesn't exist. :) https://research.fb.com/publications/moving-fast-with-softwa...

People said the same things about unit and integration tests a decade ago.

And about optimizing compilers, neural networks, and static program analysis four decades ago.

Computer science is a fast-moving field, sure. But not all of today's research bring tangible results by the end of the week, and we should be comfortable with that.

I generally agree, but formal methods I can say with confidence will get adopted in the future.

Here is why: Testing is fastly becoming adopted by everyone in our industry, why? Becuase you cannot afford to not write tests if your system is large/important enough. However our current testing methods cannot not prove the absence of bugs, as Dijkstra is fond of saying. So the best we can tell our clients currently on the bug-free/security question is this: "We wrote it according to X standard and wrote tests to cover those cases.". Formal methods allow us to prove a system is bug-free/secure. It is the evolution of testing. I do not know how far off it is, but because we have already adopted testing I believe formal methods will get adopted as well.

formal methods don't magically make a specification bug-free/secure though, nor does it mean you won't making bugs in the formal verification code you're writing.. so what are you actually proving? other than just another layer of testing essentially? can anyone tell a client that a system has been 'proven' correct? I think when we use these words with people who don't completely understand the implications we need to be more precise what that means... that's what leslie lamport is all about ! being precise!

My company still says that today. All the while saying we should do them, but not impact our velocity. Yeah, okay.

Not that unreasonable, depending on what your use case is. There are some good, very approachable guides out there like this one[0].

[0] https://pron.github.io/posts/tlaplus_part1