"most of these tools like TLA+, live in another dimension, proving something in TLA+, doesn't mean..."

This sentiment is sloppy, dismissive, with an tinge of obligation to bend to old man wisdom. I don't buy it for a moment.

Let's do better.

Formal tools help suss out requirements solved with high level algos for selected hard sub-issues of the problem under consideration. It's not code to be sure. And, this argument cuts both ways.

It's also far from a clear a pile of code knows, expresses, implements, or communicates its requirements. Just because the code compiles doesn't necessarily mean squat either.

So first thing: specification and implementation are both important and walk hand in hand. How tightly you hold onto one or both depends on several factors such as: are you competent in formal tools (learning them is tough), are there really hard sub-problems e.g. distributed computing on the table? etc.

Second, I want to deal with risk ... you know ... connecting the dots end-to-end in software from customer to requirements to coded. I'll motivate my point with a imaginary story.

In Silicon Valley two companies A, B on opposite corners of the same block are having a big team meeting. The big boss is in with important news.

Company A: We just got a huge, new sale 10x our normal size. They want our basic product but with a lot of extensions, customizations. Business will get you situated with it. Effective now we're suspending our current work. All team leads and lead techs are required to meet with business to assess work planning, risk, task order, deliverables, and so on. We expect this work to run for 18 months. In that time we may abandon, re-prioritize, and clarify work as coordinate with the customer. The customer may change their mind etc.. But as we know well, coding the product goes hand in hand with risk, discovering clearer requirements, and doing a better job of delivering them. We're equal to it.

Company B: We just got a huge, new sale 10x our normal size. They want our basic product but with a lot of extensions, customizations. Business will get you situated with it. Effective now we're suspending our current work. Part of this new work requires us to glue feedback from three controllers, plus sensors in realtime to compute steering commands to the cockpit console. If we nail this, there's 100x more work for us. Given how crucial this aspect is, we'll use Lean, Spin to model requirements and work out some LTL to make sure we're on the right path before we code. We expect this work to run for 18 months minimum. In that time we may abandon, re-prioritize, and ....

Now at this point the boss at company B is cut off with a bunch of whining from its developers:

* formal live in another dimension

* a good model doesn't mean right requirements

* even if the model is right there's no proof it's implemented right

* it'll take longer to do because we've added scope

* etc..

The boss at company A, B are both doing the right thing. Both companies have risk - a lot of it. But company A has engineers on staff who are preternaturally good at dealing with risk. Company B, unfortunately doesn't really understand risk at all in terms of doing something about it.

In this story company A never talked about formal tools. That's on purpose. I want to emphasize only that the problem to be impacted is risk levels, risk location, and sensible ways to manage it. Here formal is but a tool. It's not magic. It's just a tool. Had the boss at A mentioned formal tools, engineers would have rolled with it seeing it as one more bullet in their armory.