Surely you agree that it's possible to prove x>0 is true after executing this program:

    if(x <= 0) {
        x := 1; 
    } 
 

People have come up with techniques for reasoning about loops and recursion. Not in general, of course, but for some specific property (e.g., x > 0) and some specific loop (e.g., while(x <= 0) x := x + 1) there are techniques for proving that the property holds after the loop.

> I regularly see similar claims about software validation

Validation and verification are very different things. Verification is "my program meets these formal specs". Validation is "my specs accurately encodes the whole problem". Indeed, there's no way to do validation in a provably correct way. (But, of course, mathematics and statistics can help :-) ). The good news is that a lot of security and other bugs arise even once you have the correct spec. So verification can be useful even if it's impossible to perfectly validate.

> by people who either do not know, or who don't want to acknowledge, that this problem cannot be solved in the general case.

It's somehow ironic that you invoke the Talking problem since Turing himself -- AFTER having proven the Halting problem -- basically conjectured the creation of formal methods.

You are correct that creating a program that verifies any other program is mathematically impossible. However, given some critical assumptions regarding the scope of the problem, we can use formal verification techniques to generate proofs for some programs. People in formal verification (https://en.m.wikipedia.org/wiki/Formal_verification) do research to find better ways of creating proofs for programs automatically.

This formal verification walkthrough goes through the hows and whys of a recent project with Amazon that may have some answers for you. Obviously a different project but the fundamentals are similar https://galois.com/blog/2016/09/verifying-s2n-hmac-with-saw/ (I work at Galois)

> that this problem cannot be solved in the general case.

They are not solving it for the general case. They are solving it for many specific cases. Presented with a system, there is no guarantee that this will be possible - there can't be, that's what the Halting Problem says. But there is also no guarantee that it will be impossible for the particular system under consideration - that is not what the Halting Problem says.

Real computers are finite state machines, not Turing machines.

Correct but not relevant. No formal verification technique takes advantage of the fact that the computer has "only" 8 GB or RAM and 1 TB of disk space as its tape (~ 2^2^43 states).