The huge value that I see in a formal specification language like TLA+ is that we could have a precise way of communicating the problem in a way that is agnostic to the implementation language.

Imagine something like StackOverflow, but instead of posting a question, you post a formal spec. Thinking even further, you could then find a way to combine/interface these specs and build something like a global database of computational problems.

We're currently doing this already with StackOverflow, but we're focusing on the implementations, not the problems themselves.

Please correct me if there's a mistake in this line of thought, I'd love to know.