A lot of things wrong with your arguments. When you say correctness, you are pushing for a specific method for reducing amount of problems caused by defects, while these problems is what we actually care about when we talk about reliability, not defects, not bugs, not correctness. Yours is just one such method, and one of the expensive ones. This is very important distinction if you want to understand why "proving correctness" cannot get anywhere. For a lot of software even if we need reliability there simply exist more objectively better ways to achieve it.
Business is another thing, nobody convinced them to go along with anything, it's the other way around. Incentives to produce software the way it is produced actually come from businesses as they are the ones paying for it. Engineers just go along with it.
I get that software industry is very dogmatic and it's hard to see things for what they are. But we should at least try.
> When you say correctness, you are pushing for a specific method for reducing amount of problems caused by defects, while these problems is what we actually care about when we talk about reliability, not defects, not bugs, not correctness.
I'm using "correctness" to mean software that is bug-free.
The system that the software is a part of may still have problems, but none of those problems should be caused by bugs in the software components. It's also possible to build bug-free software that solves some other problem than the one you have. Both of those issues are orthogonal to the issue of why the industry doesn't adopt methods that generate bug-free code.
> Yours is just one such method, and one of the expensive ones.
I expect to be able to train normal, non-programmer folks to be able to use it (a HOS-like system that permits elaboration of a top-level spec into bug-free working code) to develop bug-free programs. If that works it may be so cheap that it depresses the market for "real" programmers. I should be so lucky.
But regardless, these methods (HOS, Cleanroom, etc.) just aren't that dreadfully expensive. And bug-free code, once written and paid for, can be reused. The cost analysis has been on the side of "provable correctness" for longer than my lifetime.
> This is very important distinction if you want to understand why "proving correctness" cannot get anywhere.
Well I don't accept your assumption that '"proving correctness" cannot get anywhere'. My whole point it that it has gotten places and we're all ignoring it because we prefer to use e.g. C and Java and {{POPULAR LANGUAGE}}...
> For a lot of software even if we need reliability there simply exist more objectively better ways to achieve it.
If you are talking about "reliability" of software I don't know what that means other than bug-free.
I know you can build reliable systems out of unreliable parts, but to do that there still has to be some reliable system orchestrating them and compensating for failures.
But again, I'm not saying there's a method for reliable systems, only reliable software. The absence of the former doesn't invalidate the existence or desirability of the latter.
> Business is another thing, nobody convinced them to go along with anything, it's the other way around. Incentives to produce software the way it is produced actually come from businesses as they are the ones paying for it. Engineers just go along with it.
The "suits" aren't to blame for this one. They only know what we tell them (to a first approximation.) If you tell your boss, "I can chop better with this ax than that chainsaw." you're lying or ignorant. How is management supposed to even know the possibility is there if the programmers doesn't tell them? Or they bring it up and the response is "Sure, I'd love to use {{TECH}} but {{EXCUSE}}."?
There's a cost for bugs. If you can get bug-free programs for the same upfront cost as buggy ones (and my whole argument is that we can, but don't) then there's no upside and only downside to accepting buggy software, and methods that permit buggy software to be written.
We could use chainsaws, instead we use axes and claim chainsaws are too expensive and axes cuts fine.
It's not because the bosses, who only care about board-feet[1] per worker per hour, are too cheap to buy chainsaws.
[1] "The board-foot is a unit of measure for the volume of lumber in the United States and Canada. It is the volume of a one-foot length of a board one foot wide and one inch thick. " ~https://en.wikipedia.org/wiki/Board_foot
I've never heard of many ax related deaths and I'd imagine an out of control chainsaw is far more dangerous than an out of control ax. The vast majority of lumber industry related deaths are due to falling trees. If we took the chain saws away and replaced them with axes and hand saws, far fewer trees would fall. It would greatly reduce production, but I'm not convinced it would result in more deaths. Quite the opposite.
I do get the point of your analogy, but it's really a very poor analogy.
> If you can get bug-free programs for the same upfront cost as buggy ones (and my whole argument is that we can, but don't)
This sounds like a massive market opportunity. One then wonders why absolutely no one has exploited the opportunity. There's something missing here.
(In this metaphor, you can even use your ax to carve a chainsaw out of a tree in your spare time, and then use that! But we don't. "It's too expensive."
As an example, here's a way to get Logical Paradigm programming in your favorite language http://minikanren.org/ It's simple, easy to understand and implement, and you can use it to do things like type inference and type checking with flexible and powerful constraints to define and ensure invariants and stuff like that. This stuff isn't expensive or even that challenging, we just don't do it.)
Business is another thing, nobody convinced them to go along with anything, it's the other way around. Incentives to produce software the way it is produced actually come from businesses as they are the ones paying for it. Engineers just go along with it.
I get that software industry is very dogmatic and it's hard to see things for what they are. But we should at least try.