Does this speak more to the pursuit of the application of software to problems generally or to the baseline triviality of problems that are funded to have software applied to them?
To me it seems like an incentive problem that starts with the distorting effects of unsophisticated investors w/ unrealisitic expectations who fund following a herd mentality only things they can themselves pattern-match to.
A business process that works "by itself" most of the time, but requires human intervention once in a while, is still a functional business process. The unit of "software + 5% of this person's time" is perfectly workable. And if the cost of the fix is more than the NPV of 5% of that person's time, it isn't worth making.
Catastrophic failure risk, of course, changes the analysis. But a huge range of things are not catastrophic in their failure modes.
To me it speaks of Software being "good enough" far more easily than it can be perfect.
> To me it seems like an incentive problem
Why is it a problem if a buyer gets something that works well enough for a lot less time/money put in?
Further to that - specifications and requirements are often imperfect, poorly pinned down, ever-changing. Software creation out in the commercial world has shifted working patterns to try to adapt to that (Agile methods amongst others). Attempting formal proof of such soft, malleable systems would appear to be a fool's errand.
The challenge with this formulation of "ever-changing" is that it assumes that things like Agile methods are somehow creating the capacity to iterate toward something of value with intention and ambition in such a way that you'll achieve whatever it is that you're trying to achieve.
However, what happens is that the lack of rigor in software development today seems to cause the lineage of development and associated created technology to drift further and further away from the desired commercial goal as those goals change or mutate.
Creating a bunch of brittle technology and technical debt to poorly approximate Purpose-A (a purpose by the way that you might be able to formally prove trivially is actually impossible and you either shouldn't waste the money or should intentionally select the best sub-optimal solution) doesn't help you get to Purpose-B any faster. As you become aware that Purpose-B is a thing you need to angle toward, you're still dealing with the pile of bubblegum, toothpicks, and instruction manuals written in alien script that still hasn't achieved Purpose-A.
It's a really weird thing to me that as an entire ecosystem and community we've decided that the most valuable way to approach software is to declare that it's impossible to ever "finish" it.
If I have a series of high-assurance layers to build upon that I know I can trust, then iterating and adapting to changes actually becomes faster and easier, because I know the surface area of where a problem can actually reside and how deep in any part of a system I actually have to uproot and start over. In the current formulation of the world, basically everything is a suspect, and basically any solution is considered viable... whether it truly is or not.
I've been in situations where Product Managers and Engineers spent months off and on arguing over some proposed solution or feature and never getting anywhere because everybody's basis was built on social capital, political capital, and mythology. What finally killed the conversation and allowed progress to actually happen? When a TLA+ model that invalidated one of the proposed hypotheses was presented. "Well, look. The way you want to do this is actually impossible. It will need to be done like this, this, or this instead." Seven... _seven_... sprints of about a dozen people wasted because nobody could formalize either the requirement or the approach. Until somebody did. This wasn't for a safety-critical system either.
> The challenge with this formulation of "ever-changing" is that it assumes that things like Agile methods are somehow creating the capacity to iterate toward something of value
If you're doing it reasonably well, they produce small chunks of something valuable every iteration.
> Creating a bunch of brittle technology and technical debt
Who's creating brittle software or technical debt? Things can be well designed and well written, well structured and well tested without going as far as formal proof, which in most commercial situations is going to be masses of overhead and quickly not applicable to the ever-shifting problem domain.
> It's a really weird thing to me that as an entire ecosystem and community we've decided that the most valuable way to approach software is to declare that it's impossible to ever "finish" it.
You seriously need to get out into the commercial world more. Or perhaps into the smaller, faster moving commercial world (I'm not sure where you are now).
> If I have a series of high-assurance layers to build upon that I know I can trust,
Then the underlying assumptions are likely to change, rendering your layers an expensive boondoggle.
> I've been in situations where Product Managers and Engineers spent months off and on arguing over some proposed solution
Then you have bigger problems than formal proof.
I'm generally looking at things which are designed and delivered within a number of months - anything that takes months to argue over has entirely missed the boat as far as I'm concerned.
Totes agree. Also, customers are humans. They don't want to be handed a perfect product. They want to be involved in the process. Make dumb decisions. Complain. Receive bugfixes. Repeat.
I don't know. Maybe I'm jaded, but I think in B2B, good software is not even desired. In B2C, sure, as Apple proves, but not in B2B.
You can make good software without formal proofs. It just may not be proven to be perfect.
> They want to be involved in the process. Make dumb decisions.
This I agree with though, sure. They do make dumb decisions, and they push ahead anyway, even when told. Later they change their minds, we change the software. It's the grand circle of life or something.
Commercially speaking - it's usually not.