I get what you mean, but it’s worth remembering that TLA+ is a language that is designed foremost for thinking about CS stuff, and at the end of the day, it’s “just” an improved notation for mathematics (particularly the kind of math that’s relevant for describing systems). In fact, Lamport didn’t even believe it was possible for TLA+ to practically run on a computer when he invented it (someone else did TLC).

So, here are a few reasons that recommend learning TLA+:

* If you already know how to program, you can learn it pretty quickly; almost certainly in less than a month. Just use TLC as a highly responsive yet infinitely patient teaching assistant.

* Once you learn TLA+, you’ll not only find it easier to think about systems and algorithms, but you’ll also have more opportunities to practice since you just need pencil and paper. I find myself doodling in TLA+. I'll even go so far as to say that TLA+ has a Tetris Effect[1].

* This is probably true of most esoteric technologies, but since TLA+ is pretty obscure, the community is still in that sweet spot that is the intersection of smart and friendly. Lamport answers questions in the mailing list.

* Just my opinion, but TLA+ (or something very much like it) is part of the future of CS pedagogy.

[1] https://en.wikipedia.org/wiki/Tetris_effect