> 1. How do we really get the feel for the benefits of this model? Sure, I can struggle through tutorials on TLA, white papers on Daedalus, and the Eve live dem

> 1. How do we really get the feel for the benefits of this model? Sure, I can struggle through tutorials on TLA, white papers on Daedalus, and the Eve live demo, but from the little I've seen it's not yet obvious to me how they solve my problems as a day-to-day jobbing programmer. The benefits of Haskell, on the other hand, became clear to me after browsing the Haskell Reddit and noticing that pretty much every post solved a problem I was currently having in my Python codebase. With respect to TLA+, here's how I'd say it solves problem as a day-to-day jobbing programmer: you know the saying "Weeks of programming can save you hours of planning?" TLA+ is a tool to make planning less tedious and error prone. You can write your plan as a specification, then check if that specification actually meets your required invariants. If you're expecting to write a couple dozen lines of code, TLA+ is probably not gonna help a lot. If you're expecting to write a couple thousand lines of code, it can save you a ton of pain. But you still have to implement your specification correctly, and that's where things like ADTs can help quite a lot.