aychtang
Joined 8 years ago
Karma
9
Submissions
6
Member since
Dec 3
My email is my username at googles email service
View on Hacker NewsRecent submissions
Comment · 5 years ago
Ops
Comment · 6 years ago
Are there benefits of being Startup School Certified? It's not clear in the FAQ
Comment · 6 years ago
Yes apart from it's not pseudocode but mathematical formulas.
Your building blueprints aren't made from bricks and mortar because it would just take way longer and be expensive to experiment with, however with software when designing we often use the same tools as building without thinking of the cost like that.
TLA+ and other lightweight modelling languages allow you to experiment with your design and verify that it works without all the tedium of programming languages and their environments / libraries / compilers etc.
Comment · 6 years ago
TLA+ was created so you can quickly model / specify a design, check it works under your assumed invariants and maybe explore alternatives up front, giving you a plan for how your system should work in theory.
Like you mentioned it's the software blueprint, and you go from a blueprint to a building by actually building the thing - TLA+ is not made to codegen your product.
Comment · 6 years ago
Hillel Wayne (who wrote this guide) also has a great blog with many posts related to this topic: https://hillelwayne.com/
Leslie Lamport (who created this language, has written many seminal papers on distributed computing and is a Turing award winner) has also published an excellent book and video series introducing the design and practical usage of TLA+, you can find the video series at: http://lamport.azurewebsites.net/video/videos.html