This is relevant for security, because entire operating systems have been formally proven to adhere to their specification/free of all bugs: https://en.wikipedia.org/wiki/L4_microkernel_family#High_ass...
2. Even proving anything about finite state machines is NP hard so the problem is harder than just using weaker model of computation.
3. Proofs are not reuable: proving something about one program does not tell us anything about other programs.
See excellent https://pron.github.io/posts/correctness-and-complexity for more details.
> 1. Unfortunately the set of "some" programs is unknown and most probably really small.
Many useful algorithms can be proven to terminate. Compare against the situation in mathematics: many theorems are not be provable, but that does not stop us from trying to prove useful theorems, or recognizing that a given theorem has already been proven.
> 3. Proofs are not reuable: proving something about one program does not tell us anything about other programs.
This is true in the sense that a proof of arbitrary program A does not tell us anything about many other programs. But it is clear for example that if, say a program is recognized by inspection as the concatenation (splicing the final states and initial states together) of two programs that terminate, then this program terminates.
Even the link you provide gives optimism and claims that
> Now we know why writing correct programs is hard: because it has to be. But while we cannot verify all programs all the time – regardless of how they’re written – there’s nothing stopping us from verifying some programs some of the time for some properties.
I would say that one small piece of software (Sel4 is only 9,400 SLOC!) always cited as an example is actually a very small set of programs that can be formally verified. I haven't heard of a formally verified web browser...
> Many useful algorithms can be proven to terminate.
Proving that a program terminates is not that much interesting. Lack of security vulnerabilities would be much better.
> But it is clear for example that if, say a program is recognized by inspection as the concatenation (splicing the final states and initial states together) of two programs that terminate, then this program terminates
But it does not tell us anything about real programs? We don't compose software by concatenating their state machines.
> Even the link you provide gives optimism and claims that
This is a call for empiricism (aka testing) and ad-hoc heuristics exactly because the problem is not solvable in general using formal methods.
> Proving that a program terminates is not that much interesting. Lack of security vulnerabilities would be much better.
My bad, I dare make the stronger claim that most algorithms that you see in an undergrad algorithms textbook are useful and mathematically known to be correct.
> But it does not tell us anything about real programs?
I agree that most software today are extremely complicated. Most software today don't even have a proper target specification all in one place, which is kind of a prerequisite for being proven to adhere to a specification. Furthermore, most software today is so complex that attempts at a rigorous specification is likely to have bugs at the level of stating the property itself. Not to mention completely missing properties that one is unaware of that are relevant to attacks that one is unaware of.
But core parts of real software is composed of those undergrad algorithms that are proven to be correct. You can create useful libraries of useful algorithms that have guarantees, and small programs that have guarantees. For this reason I disagree that the class of useful programs is as small as you think.
> We don't compose software by concatenating their state machines.
Structured programming without loops can be modeled as concatenation of turing machines (branching composes different machines to the accept and reject states); and it is trivial that it terminates once the component machines terminate.
When you introduce a loop that is when you need to identify a nontrivial property that guarantees that the loop terminates, and this is done work for many useful algorithms.
They are reusable to some degree when the proofs are made with type systems, via Curry-Howard.