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.
What you're talking about there is a Model Repository. We're building one at the bank I work at, except because our modelling language (or meta model) is based on OMG's MOF we can generate artifacts (code) from our models. You can't do that with TLA+ as far as I know. It's pretty powerful - you can compose models together very easily, as well as generate loads of useful things for data-in-motion.
Hey, thanks a lot for your response! It's really hard to search for abstract ideas like this if you don't know the terminology (like Model Repository), so this is super helpful. This is a very interesting topic for me, may I ask you a few questions? I sent you a request on LinkedIn.
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.