The linked paper is quite interesting [0]. It does indeed sound like TLA+, the formal methods tool set they used, has worked out very well. One quote: "[W]e have found that software engineers more readily grasp the concept and practical value of TLA+ if we dub it: <i>Exhaustively-testable pseudo-code</i>. We initially avoid the words ‘formal’, ‘verification’, and ‘proof’, due to the widespread view that formal methods are impractical."<p>[0] <a href="http://research.microsoft.com/en-us/um/people/lamport/tla/formal-methods-amazon.pdf" rel="nofollow">http://research.microsoft.com/en-us/um/people/lamport/tla/fo...</a>
Here's an interesting blurb about how they were using TLA+. TL;DR is is that, unsurpisingly, model checking trumps proving in roi:<p>We have found formal specification and model-checking to yield high return on investment. In addition
to model checkers, many formal specification methods also support formal machine-checked proof.
TLA+ has such a system. The TLA+ proof system has several compelling benefits; for example, it supports
hierarchical proof. After doing only a small number of such proofs, author C.N. has found that
hierarchical structure is an effective way to handle the otherwise overwhelming amount of detail that
arises in formal proofs of even small systems. Another benefit of the TLA+ proof system is that it takes<p>as input the same specification text as the model-checker. This allows users to find most of the errors
quickly using the model-checker, and switch to the proof system if even more confidence is required.
Even though formal machine-checked proof is the only way to achieve the highest levels of confidence
in a design, use of formal proof is rarely justified. The issue is cost; formal proof still takes vastly more
human effort than model-checking. We are continuing to experiment with the TLA+ proof system, but
currently model-checking remains the sweet spot in return on investment for our problem domain. We
suspect that proof will only be a worthwhile return on investment for one or two of the most critical
core algorithms.
r/programming discussion of this paper here: <a href="http://www.reddit.com/r/programming/comments/277fbh/use_of_formal_methods_at_amazon_web_services/" rel="nofollow">http://www.reddit.com/r/programming/comments/277fbh/use_of_f...</a>
The Envisage Research Project - <a href="http://envisage-project.eu" rel="nofollow">http://envisage-project.eu</a> - is working on developing formal methods for software engineering for the cloud, ref: <a href="http://envisage-project.eu/wp-content/uploads/2013/10/Envisage_factsheet.pdf" rel="nofollow">http://envisage-project.eu/wp-content/uploads/2013/10/Envisa...</a>
"ENVISAGE will create a development framework based on formal methods to include resources and resource management into the design phase in software engineering for the cloud. This will improve the competitiveness of SMEs and profoundly influence business ICT strategies in virtualized computing"
I have used Computational Tree Logic before (<a href="https://www.firebase.com/blog/2014-02-04-firesafe-complex-security-logic-for-firebase.html" rel="nofollow">https://www.firebase.com/blog/2014-02-04-firesafe-complex-se...</a>)<p>I wonder if anybody knows what the main differences between CTL and TLA are. Maybe I should switch camps?<p>EDIT: oooh, you can read the book for free <a href="http://research.microsoft.com/en-us/um/people/lamport/tla/book-02-08-08.pdf" rel="nofollow">http://research.microsoft.com/en-us/um/people/lamport/tla/bo...</a><p>EDIT2: Ahh... TLA has sets for one thing
Can someone explain give an introductory run down on model checking vs theorem proving and why someone wouldn't just want to write these systems/algorithms in a dependently typed language?