I misunderstood the goalposts because you had seemed to be talking about theoretical CS notions like complexity and computability (we were talking about the halting problem), and now you are talking about proving properties motivated outside TCS.

> 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.