alt Hacker NewsWhile 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.