Going off on a tangent, but If I were to reduce TLA+ to a (perhaps obscure) buzzphrase, I’d say it is “theory B for (and by) theory A people”. This is felt not only in the choice of the extremely general computational model of abstract state machines as opposed to some more specific algebra (or “calculus”), but also in the emphasis on and interest in how “plain engineers” can (and do) put it to use in practice. I think that this emphasis (and even interest) is sorely lacking in some of the theory B work, which may result in the real-world efficacy of some of its most interesting work remaining forever unknown.
While it is true that TLA+ is completely orthogonal to PL concerns, I do think that there is some real competition here, certainly in the approach (and I’m sorry if I’m stirring a pot which should not be stirred). Even though TLA+ is a formal language, I think — and correct me if I’m wrong — that it is firmly in the verification camp, which basically says “express your program how you like, we’ll give you tools to reason about it”, while the PL camp says, “we’ll give you tools to express programs in a certain way, and if you do, they’ll be easier to reason about”. I guess that the PL people would say that their very approach would inevitably result in fewer of their attempts being adopted (it’s easier to adopt a tool that fits how you already work, than a tool that requires you to change how you work to fit with it), but they hope that those few ideas that eventually do get adopted would have a long lasting, revolutionary impact. In a way, it is a competition between pragmatists and idealists, I think. As a "plain engineer" practitioner, I, for one, would be very interested in seeing a panel discussion between the two different camps.