[sirmarksalot]

I think that's one aspect of the problem, but the migration from make-do to mathematically rigorous code can be equally fraught with peril. While the code itself can be made predictable, and easy to reason around, the time estimates and project planning often cannot. There is never enough time to factor out all of the commonality, remove all of the unnecessary use of state, codify all the assumptions into data types, etc., so you have to pick your battles.

A programmer needs intuition of what the biggest, most effective improvements are on the code base, which allow them to get the most work done. They also need some ability to guess how much time it will take, so that they don't miss deadlines. No amount of static type analysis will fix that.

[Refefer]

Ah, but that's a matter of design - except now we have strong constructs from which to consider our problem. We will never get away from developing the architecture of our system, which is cost dependent on how well understood the domain is. Ideally, that's where we should aim to move: problem specifications that render implementations rote. A lofty goal, I know, but within closer reach every day and possible in many environments already.

Part of the beauty of proof is that so long as it is correct, the individual lemmas are largely irrelevant: we don't necessarily need to remove commonality or statefulness. Of course, I'm purposefully glossing over extra-functional requirements on which, outside of big-O, we don't have a firm grasp.

I'm attempting to stay away from "effective" or "most work done" since they're ill defined and highly subjective but rather focus on measurable changes. I'd argue that, amortized, the upfront costs of better understanding the problem definition results in cost savings down the line, especially as it recedes into maintenance.

[sirmarksalot]

The dark side proof is that most mathematical problems are incredibly contrived. Taking a business requirement and translating it into known mathematical problems is harder than it sounds. Once you can do that, you're 90% of the way there, and people who can do that reliably are regarded as geniuses.

But most of the time, development is done without full understanding of the problem space. Usually, the problem doesn't become fully understood until you've already spent a good amount of time coding up your solution. If you wait until you fully understand the problem before starting, then you'll never start, because your brain simply can't comprehend the entire scope.

So instead, you get code bases full of sort-of well-factored code, but with lots of unwittingly reinvented wheels. This status is occasionally improved when somebody really smart happens to notice the commonality, and remembers a classic problem that it resembles, and manages to refactor the entire thing using the general solution. However, this almost never becomes apparent during the first revision.