aychtang

Ops

Are there benefits of being Startup School Certified? It's not clear in the FAQ

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.

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.

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