The number of people in industry who use either tool is incredibly small and is likely to remain so; developers spend 20-50% of their time on test suites and STILL don't feel it's cost-effective to write down formal specs, even in TLA+-style specifications.
What matters is that important libraries and frameworks can be verified, not that everyone and his brother can use formal methods for every WordPress website they churn out.
How many zero-day security flaws have to occur in core infrastructure like, for instance, OpenSSH before the laziness of engineers about learning "academic" tools stops being a cost-effective excuse not to use formal methods?
I agree, but I see some chance of TLA+ of getting wide(r) adoption, precisely because it is rather easy to learn and uses math that most engineers are already familiar with. Also, it allows gradual verification: specification -> model-checking -> proof (with each additional step being completely optional)
> not that everyone and his brother can use formal methods for every WordPress website they churn out.
I don't know about WordPress websites, but Amazon engineers do use TLA+ to specify many (most?) AWS services.
Also, formalizing architectural properties for the world's most popular cloud service is probably even rarer a task than formalizing language specifications.
English usage note: if the word you meant to use was "disingenuous", I would suggest "spurious" instead, as it expresses similar feelings about "this distinction", without also attributing unsavory motives to 'pron.