While I completely agree with 3uru, where it can get stuck is if your system contains a pseudorandom generator or some other cryptographic shenanigans. These are programs deliberately made difficult to analyze and reason about.
I would say, in practice, you are more likely to encounter complexity barrier (we don't know how to decide some NP-hard problem fast enough) to proving things about your program than you're to encounter a true undecidability barrier (Rice theorem).
That's a good point, although couldn't you usually black-box those and assume the invariants we expect of those primitives are in fact true? E.g. you don't need to bother trying to prove properties about your prng itself, you can just prove how your program behaves under a random oracle model.
If you're able to detect where you use these hard-to-analyse functions, then yes. This is feasible on source level, and maybe known compiler binary level. I think ultimately people will want to validate properties of binary code against the model specification of their hardware.
Although the prover might be smart enough to say, "this function is getting kinda complicated, let me model it as a random variable and see if it's enough". I think LLMs can kinda do it but not sure if your typical theorem provers can (it's on the level of being able to employ probabilistic proof techniques).