Pinboard (jm)
https://pinboard.in/u:jm/public/
recent bookmarks from jmUse of Formal Methods at Amazon Web Services2014-06-17T13:33:47+00:00
http://research.microsoft.com/en-us/um/people/lamport/tla/formal-methods-amazon.pdf
jm
The success with DynamoDB gave us enough evidence to present TLA+ to the broader engineering community at Amazon. This raised a challenge; how to convey the purpose and benefits of formal methods to an audience of software engineers? Engineers think in terms of debugging rather than ‘verification’, so we called the presentation “Debugging Designs”.
Continuing that metaphor, we have found that software engineers more readily grasp the concept and practical value of TLA+ if we dub it 'Exhaustively-testable pseudo-code'.
We initially avoid the words ‘formal’, ‘verification’, and ‘proof’, due to the widespread view that formal methods are impractical. We also initially avoid mentioning what the acronym ‘TLA’ stands for, as doing so would give an incorrect impression of complexity.
More slides at http://tla2012.loria.fr/contributed/newcombe-slides.pdf ; proggit discussion at http://www.reddit.com/r/programming/comments/277fbh/use_of_formal_methods_at_amazon_web_services/]]>formal-methods model-checking tla tla+ programming distsys distcomp ebs s3 dynamodb aws ec2 marc-brooker chris-newcombehttps://pinboard.in/https://pinboard.in/u:jm/b:8758e4d5f996/