Serious question: do you really believe that?
> That's just stupid. Show me the studies.
There is a kind of HAL-9000 quality to many of these arguments. Formal verification is perfect by definition. The fact that it hasn't had very much impact in the real world is all the more evidence of the world being full of wicked people.
I mean it's a fact, so yes. You can prove programs are correct. The only possible flaw they can have is the specification is wrong.
> The fact that it hasn't had very much impact in the real world is all the more evidence of the world being full of wicked people.
That's very much not what I said. There may be many reasons. Assuming some conclusion without actual research is braindead. Cost-benefit analysis is not the only reason things do/don't happen in businesses and we have no idea whether that's the reason here. It's an empirical question that requires actual research, not a priori jacking off.
So specifications are kind of like programs?
Have you heard of logical positivism?
> That's very much not what I said. There may be many reasons.
My point was that it always seems to be some external factor. That strikes me as being very convenient.
> Assuming some conclusion without actual research is braindead.
I didn't think I assumed anything. Like anybody else, I have many things that I need to assess in my day to day life, and often deal with considerable uncertainty.
Formal verification shines in two situations: complicated optimized algorithms with a naive reference implementation you want to confirm equivalent, and high-level behavioral invariants of complex systems (like seL4's capability system, or a cluster database's consistency during literally all possible failover scenarios).
I'm guessing you know this but in type theories like Agda you can just specify that the input and output to an algorithm has the desired properties, rather than needing to specify any reference algorithms. For example, you can just state that an implementation takes a list of X and that it outputs a sorted list of X. Nothing more is necessary in cases like that in such a system, no code, just the single type.
And the reference for "sorting" could likely be a deterministic bogosort and certainly a primitive bubblesort.
Even if you're just looking at sorting stability, you're past what your simple "sorted" type would cover.
Most things are far less trivial than "sorted list", including (almost?) all interesting practical applications of formal verification in the life of a "normal" software engineer.