Looking at the discussion around your and Turing_Machine's points, I think one could generalize the problem like this: in a large and complicated search space, finding a solution is much faster and cheaper than trying to comprehend and formally describe the search space (to later derive the solutions). The up-front costs of doing the latter are so high (I don't think we even have a good bounds on them) that nobody who needs a solution bothers with it. Iterative search is the only way individuals and teams can feasibly find the solution they're looking for.

This way, I think formalizing software development is a worthwhile goal - just like formalizing cooking is - but it's also obviously so uneconomical that we can't expect the industry to bother with it. Formal methods are pretty much basic research - not useful for us in any meaningful timeframe, but hopefully our grandchildren will get some mind-blowingly amazing tools out of it.