Coding is the process of fully understanding what needs to be built. We've all seen architecture astronauts churn out reams of UML that still result in a broken system. Exploring the space via iterative MVP is far more productive.
> Coding is the process of fully understanding what needs to be built.
Not every domain affords you the luxury of coding the wrong thing and then fixing it in a later iteration. Sometimes due to financial constraints, other times because people wouldn't exactly be okay with the 0.7.1 version of your plane software leading to crashes until the next patch.
That said, i somewhat agree with you that UML and abstractions can only lead to problems if there's too many of them. A few high level overview diagrams can be good to have, but only as long as they conform to the actual architecture and models 1:1, and as long as they're not made at the expense of actually writing working software and perfecting it.
However, as long as only one person with incomplete knowledge of the domain or requirements is the one to write the code, you'll still end up with sub par solution. Personally, i think that the only way around that would be a paradigm shift of sorts - instead of planning meetings that aren't good enough, you might as well do programming meetings and mob programming in which you'd code the most important architectural bits of the software that you need, leaving the legwork for individual contributors later.
In my experience, code review is far too late for serious decisions to be made. At best, the reviewer will need to wrangle with hammering your sub optimal code into shape, at worst they'll just be like: "Sure, this looks like Java, it can go into the main branch. QA can figure out whether it's good enough or not."
The best application for formal proof is actually in lightweight sanity checks as opposed to "deep" review of your code. To put it very clearly, it should simply not be possible for a properly-engineered program to conflate feet w/ meters and crash a space probe as a direct result of that conflation. There's just no way that this is ever valid semantics.
interestingly, that's one of the areas where Ada shines, as you can define your own integer subtype that will help you preserve the semantics (and Ada has, iirc, no implicit casts, so it would require explicit cast to push feet into metres (and it might be made so that such cast would actually convert the values properly)
> But when your deployment costs run into the 7 to 10 digit numbers
That's when you throw things into simulation and do some Hardware-in-the-Loop testing. If I learned anything from studying the failure of Ariane V flight 1, it's that while analysis can be useful, testing is usually even better.
This should be normal practice IMO.