The advantage of a "safety net" has a big fight on his hands against the big disadvantage of "who's going to maintain this shit when that rock-star theorem guy is gone?". Or the theorem guys are very expensive in the first place, so it's cheaper or easier to hire multiple people who have to use unit tests like everybody else.
So eventually if - a language but more importantly - an ecosystem like that will get leverage, every existing ecosystem can slowly fade into that and develop further in this path.
At the end (almost all) programmers are going to write proofs, because this is what works in scale.
Please correct me if I am wrong!
We're currently the early explorers of a field, mostly composed practices & tips and tricks that we think help but can't be sure. We're like barber-surgeons before it turned into a true profession.
I believe we have plenty of examples today of “we can’t fire this employee because a few years ago we made a mistake of that hire and now they are the only ones who know how that pile of shit works”.
At least with theorem provers the transparent knowledge of the broken systems can be formalized.
At this point, I think the rockstar theorem guy would not be working on some proprietary business logic that needs to be maintained wholly in-house. He'd be in charge of more critical infrastructure in widespread use. Kernels, SSL libraries, optimizing compilers; that sort of thing.
As for who should hire him? I'd hope one of the big tech companies would want a project like this.
That's because the field is still in an exploratory and research phase. Unless you're in an industry where correctness is the most important criteria or involved in research into this stuff, your average programmer isn't going to be using any of this. It's still too early, but that doesn't mean it's a waste of time.
For most of the cases where formally verifying _designs_ is important (most of the industry), formal specification languages are 1) not actually that hard to learn, and 2) exist distinct from the code, so you can throw them all out if you really need to and go back to flying blind.