5 ms·
> maybe it is something to look into for cars, airplanes, medicine, etc. For the rest of us, who still wrestle with complexity but probably would't accidentally
by hwayne 9y ago
> maybe it is something to look into for cars, airplanes, medicine, etc. For the rest of us, who still wrestle with complexity but probably would't accidentally kill someone, here are some simpler aids:
TLA+ isn't perfect, but it's actually not that hard to use! I'm a webdev and it comes in handy all the time.
> Data-driven programming. I'll just quote some really smart people:
You might want to check out Alloy. It's a formal spec language that specializes in verifying data structures.
- katelynsills 9y agoCan you expand on your process for using TLA+ in web development?
- hwayne 9y agoSure! 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 agoPrevious HN discussion: https://news.ycombinator.com/item?id=14221848 https://news.ycombinator.com/item?id=14221848
- katelynsills 9y agoThanks!
- combatentropy 9y agoIs 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 agoYeah, TLA+ just verifies the spec, not the actual code. You still need to write tests and use code review and the like.
- combatentropy 9y agoOkay, that makes sense. Thanks!