Formal validation are perfect for when you know exactly what problems you're solving. Unless a business is offering a very specific solution like that, then it won't help them. If you're writing security software or low-level system controls or something. But if your customers aren't actually engineers themselves, formal validation is unnecessary and inefficient.
>There are plenty of open-source tools for using languages like TLA+ that work great besides!
Does your team know TLA+? Is it an efficient use of their time to learn it? Are a bunch of TLA+ beginners going to crank out properly written software?
They're good evrn for exploration if you're using formal specs. Reason is good ones knock out errors due to English ambiguity and inconsistencies. Z, Navy's SCR, B method, and Statecharts were all used for these purposes with success. Executable specifications did even better for exploration aspect.
Current research is taking it further with code generation from specs like AADL, UML, and especially SCADE/Esterel.
> 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.
> I could just write the code for that but I'll never prove the system works that way.
Or you could just prove from first principles, like we all learn in formal algorithm design theory.
The question is not whether proofs are valuable, the question is whether translating a system into TLA and using that proof checker is more reliable and saves you time over just attempting a proof directly.
Even if your TLA proof checks out, it may be a false positive because it doesn't accurately reflect your production code.
By all means write your proof whichever way you see fit.
What TLA+ and other languages give you is an automated theorem prover or model checked that usually is built on some form of temporal logic and predicate calculus. This is especially good at modelling multiple communicating processes. Taking a logical approach to discrete maths has a few benefits here.
> Even if your TLA proof checks out, it may be a false positive because it doesn't accurately reflect your production code.
This is something one needs to be concerned with when writing high-level, abstract specifications. There's no way yet that I know of where we can synthesize the program from the specification although I am aware of research in that regard. However we can still gain the benefit of well-defined invariants and pre/post-conditions that we can use in testing our implementation. For now your implementation will be separate from your spec but you gain insights from the spec you would not otherwise if you had only written code.
update as to whether it is an efficient use of time to use a model checker or automated theorem prover... Well I think the reason for their invention was to specifically to handle the tedious task of proofs in formal maths. Some operations are tedious and mechanical and computers are better suited to the task than humans.
One area I find interesting is languages with dependent type systems like Agda and Idris. It seems like we're not too far away from being able to model and prove our specifications directly in the type system alongside the program that implements it.
>There are plenty of open-source tools for using languages like TLA+ that work great besides!
Does your team know TLA+? Is it an efficient use of their time to learn it? Are a bunch of TLA+ beginners going to crank out properly written software?