Earlier quoted context omitted.
Can you expand on your process for using TLA+ in web development?
Sure! I've written a quick demo here[1] and a longer-form piece here[2]: [1] https://www.hillelwayne.com/post/modeling-deployments/ [2] https://medium.com/espark-engineering-blog/formal-methods-in...
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.