> Formal validation are perfect for when you know exactly what problems you're solving.
Or you're at the point where formal validation is a requirement.
There's nothing stopping one from using any of these tools as design tools. I'm working on a problem to check whether items delivered by a single producer on a FIFO queue with N workers can guarantee all work items will eventually be attended to. I could just write the code for that but I'll never prove the system works that way. The best one can do is gain confidence that for the prescribed scenarios it will work. You can get good coverage and use all of the tools we know to release something others may decide to use... but then you'll be fixing your errors after the fact when they are discovered and reported by your users. Or in the case of a system as large as AWS you may find that obscurity is no longer a comforting buffer... 1 in 100000 becomes a frequent occurrence.
update: There's nothing preventing you from only using formal methods on the critical parts of your system where a high degree of reliability is useful. One does not need to formally verify everything to gain the benefits.
> But if your customers aren't actually engineers themselves, formal validation is unnecessary and inefficient.
I think it depends on the difficulty of the problems you address with your software. If you're just sorting some lists or making system calls you might not want to bother. However if you want to guarantee consensus in the face of delays and partitions you'll need more than code to make any strong claims of efficacy. And if the public interest relies on your system I think it's necessary to serve them in the best capacity using the state of the art tools.
> Does your team know TLA+? Is it an efficient use of their time to learn it?
No. They could pick it up in a couple of weeks if necessary. It is an efficient use of their time: fewer bugs at scale means less downtime and less time spent chasing errors that slipped through.
> Are a bunch of TLA+ beginners going to crank out properly written software?
Are a bunch of beginner programmers going to crank out properly written software? There are different levels of experience and skill on any team. With training and diligence even beginners can learn to adopt the skill and ability to recognize when and where to use high level specifications and how to abstract systems into mathematical models they can test and prove.
Until then I suppose we have to live in a world where security breaches are common and the recall rates on cars will continue to increase as unreliable software continues to cause failures, lives, etc.
