After years of working on distributed systems I still keep being surprised by how easy it is miss potential outcomes. The state space is too vast for the human brain.
-
-
-
Replying to @itraor
It's a good question. For some constrained problems yes. However most systems are so large it is not practical to use formal methods on them all.
1 reply 0 retweets 11 likes -
TLA+ has been successfully used on large, real world systems. Not only is it practical, but it has been found to reduce total cost.
1 reply 0 retweets 5 likes -
That's interesting. I'd like to know more. Maybe
@hillelogram knows of some larger scale endeavours too?3 replies 0 retweets 2 likes -
We wrote about our experiences with TLA+ on large systems at AWS a couple of years ago: http://lamport.azurewebsites.net/tla/amazon.html Since then, many teams in AWS have continued to use TLA+, and had a lot of success.
1 reply 0 retweets 8 likes -
Replying to @MarcJBrooker @mjpt777 and
Teams at AWS have also used formal reasoning on critical code (like S2N https://aws.amazon.com/blogs/security/automated-reasoning-and-amazon-s2n/ …), to help reason about security properties (https://aws.amazon.com/blogs/security/protect-sensitive-data-in-the-cloud-with-automated-reasoning-zelkova/ …) and many other places.
2 replies 0 retweets 7 likes -
Replying to @MarcJBrooker @mjpt777 and
The state-space size problem that
@mjpt777 pointed out is one of the reasons I've personally found formal methods so useful. I've also found that Pluscal and TLA+ code make great precise documentation of protocols, and are great languages for rapid protocol protyping.1 reply 0 retweets 9 likes
There's a nice feedback loop too; modeling and verification makes you really keen to minimize your state space in the first place.
-
-
Replying to @colmmacc @MarcJBrooker and
I found formal methods (Z) useful to get another perspective but have not tried at scale or with TLA+. Maybe it is time to give TLA+ a try.
1 reply 0 retweets 0 likes -
If you do, check out
@hillelogram's book "Practical TLA+". It's a great intro.1 reply 0 retweets 3 likes - 1 more reply
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.