3 ms·
Thinking for Programmers (2014) [video]
- dang 6y agoSome past threads: Thinking for Programmers (2014) [video] - https://news.ycombinator.com/item?id=9353908 https://news.ycombinator.com/item?id=9353908 - April 2015 (11 comments) Leslie Lamport: Thinking for Programmers [video] - https://news.ycombinator.com/item?id=7533938 https://news.ycombinator.com/item?id=7533938 - April 2014 (32 comments)
- melling 6y agoHe mentions TLA+ is used at Amazon. Can anyone comment on its use there or anywhere in 2021? Has it gained any traction? Any other options in which to write specifications?
- captn3m0 6y agohttps://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf https://lamport.azurewebsites.net/tla/formal-methods-amazon.... mentions bugs found across S3,EBS,DynamoDB. A few other references: - https://gist.github.com/MattPD/71b63a3e1600c2b52e1db80fa2834e60 https://gist.github.com/MattPD/71b63a3e1600c2b52e1db80fa2834... (Formal Methods and Program Analysis in Industry, has lots of links on other industry usage) - https://d1.awsstatic.com/Security/pdfs/One_Click_Formal_Methods.pdf https://d1.awsstatic.com/Security/pdfs/One_Click_Formal_Meth... - https://d1.awsstatic.com/Security/pdfs/Continuous_Formal_Verification_Of_Amazon_s2n.pdf https://d1.awsstatic.com/Security/pdfs/Continuous_Formal_Ver... (Coq, not TLA+) - https://aws.amazon.com/security/provable-security/ https://aws.amazon.com/security/provable-security/
- redis_mlc 6y agoA few groups, out of hundreds.
- matthewaveryusa 6y agoI have a lot of respect for Leslie Lamport, and I've read quite a few of his papers, but I'm a little reluctant to take his advice to heart here. I think his Paxos paper is a good read, but at the end of it you understand his thinking but are no closer to writing a valid paxos system. In contrast, take Diego Ongaro's raft paper and you leave with a deep understanding of the thinking and a way to start your journey into making the thoughts concrete.