4 ms·

Can you expand on your process for using TLA+ in web development?

• hwayne 9y ago
  Sure! I've written a quick demo here[1] and a longer-form piece here[2]: [1] https://www.hillelwayne.com/post/modeling-deployments/ https://www.hillelwayne.com/post/modeling-deployments/ [2] https://medium.com/espark-engineering-blog/formal-methods-in-practice-8f20d72bce4f https://medium.com/espark-engineering-blog/formal-methods-in...
  • ScottBurson 9y ago
    Previous HN discussion: https://news.ycombinator.com/item?id=14221848 https://news.ycombinator.com/item?id=14221848
  • katelynsills 9y ago
    Thanks!
  • combatentropy 9y ago
    Is TLA+ pseudocode? It doesn't actually do anything, right? Your example with updating servers, it will never actually update the servers, right? After you try it out in TLA+, you still have to write the real code in some other language, like Bash. If so, then isn't there still a risk of bugs in your Bash program, from typos, leaving out something from the TLA+ plan, or otherwise miscopying it? If so, TLA+ does less than I thought. But I can see how it might be useful to work out a complex algorithm and scan it for holes.
    • hwayne 9y ago
      Yeah, TLA+ just verifies the spec, not the actual code. You still need to write tests and use code review and the like.
      • combatentropy 9y ago
        Okay, that makes sense. Thanks!