> The correctness function of most software is how much users want to use/pay for it, which is a pretty fuzzy problem.

This is indeed a problem, but we (well we humans, but also agents) correct this by introducing partial verifiers like tests, running lints, type checkers, etc that both verify that at least some requirements are met, and also verify that the software is internally self-consistent. And more importantly, breaking down the software into small modules that are more clearly defined

The task to get user requirements and decide the right architecture requires more creativity and is fuzzier than implementing each module. Perhaps over time there will be models specialized for each task.

And actually this approach mirrors math, if agents ever develop new math on the fly to solve a problem. Developing new math is analogous to deciding how to break up the software in modules (and also analogous to designing a language, if we subscribe to the SICP notion that libraries actually are mini-languages on their own)

That is, LLMs for math is still in the phase where they are used to prove stuff (which by Curry-Howard, is like writing code), rather than deciding what to prove (which is like deciding the signatures of each function, again by Curry-Howard)