IMO, the time of "code as math" is over. No sufficiently large software system that interacts with the real world is provable to be correct like a mathematical statement is. They are all complicated, engineered systems that are backed by a mix of formal guarantees, earned design principals, experimental testing, rules of thumb, acceptable performance envelopes, etc
This is what all software will become, down to the smallest script. The vast majority of software does not need to be provably correct in a mathematical way. It just needs to get the job done. People love the craft of programming, so I get it, it's uncomfortable to let go.
But what is going to win out in the end:
- An unreadable 100K loc program backed by 50K tests, guaranteeing behavior to the client requirements. Cost: $50K of API tokens
- A well engineered and honed 30K loc program, built by humans, with elegant abstractions. Backed by 3K tests. Built to the same requirements. Cost: $300K of developer time.
If I am a consumer of software, and not particularly interested in the details, I am going to choose the option that is 6x cheaper, every time.
This is what all software will become, down to the smallest script. The vast majority of software does not need to be provably correct in a mathematical way. It just needs to get the job done. People love the craft of programming, so I get it, it's uncomfortable to let go.
But what is going to win out in the end:
- An unreadable 100K loc program backed by 50K tests, guaranteeing behavior to the client requirements. Cost: $50K of API tokens
- A well engineered and honed 30K loc program, built by humans, with elegant abstractions. Backed by 3K tests. Built to the same requirements. Cost: $300K of developer time.
If I am a consumer of software, and not particularly interested in the details, I am going to choose the option that is 6x cheaper, every time.