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.
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.