I've read Hillel Wayne's "Practical TLA+", which is a very good introduction, and watched a couple of talks on it. I also collect case studies of TLA+ usage. I

I've read Hillel Wayne's "Practical TLA+", which is a very good introduction, and watched a couple of talks on it. I also collect case studies of TLA+ usage. I find the concept really a good idea and would love to use it more. My main issue is that because it's not an everyday tool and has somewhat complex semantics, it becomes hard to use. The syntax and tooling are quite arcane and different from everyday programming languages. That's particularly problematic as it is supposed to be a tool to think about complex issues with it. Translating back and forth between what a spec says syntactically and what it actually means semantically is just hard, and for a non-everyday user, I would expect to make more mistakes when writing a spec or interpreting one I wrote 2 months ago, than I will have with less formal methods that I can actually understand. I wish this was easier and I suspect that having a more mainstream way to express things in TLA+ would get into that direction. I tried to write a toy parser for a language that translates to TLA+, but I didn't get very far yet.