Computational hardness of "real" computer programs I have often heard it said that you cannot write a program to catch bugs in a web browser, or word-processor, or operating system, because of Rice's Theorem: any semantical property for a Turing-complete language is undecidable. 

However, I am not sure to what extent this applies to real-world program likes operating systems. Do these types of programs need the full strength of Turing completeness? Are there simpler models of computation (such as PR) in which these applications could be written? If so, to what extent does this allow decidability of program correctness?
You certainly can write programs which catch bugs -- there is a large and active community of people who write programs to do exactly that. However, what Rice's theorem prevents you from doing is to write bug-catchers which are both sound and complete (i.e., catch all bugs of a certain class with no false positives). 

That said, naive restrictions on the model of computation don't actually help you very much in improving the practicality of program analysis. The reason is that you can get programs which do "almost the same thing" by turning while loops

while P do 
   C


into for-loops with a big iteration constant:

for i = 0 to BIGNUM do 
  if P then 
    C
  else
    break


Now this program does not even need the full strength of primitive recursive (since the for-loop can be macro-expanded into a huge nested if-then-else statement), but in most practical cases it will behave just the same as before. Note that it does help decidability in theory -- the program is total, so you can answer questions by running the program and seeing what happens. This is not  what we actually want, which is to get answers faster than running the program -- the artificial termination introduced doesn't actually help program analysis in practice, since bugs occur because of errors in the real program logic, and we haven't touched that at all. 

Furthermore, adding abstraction facilities to a programming language can radically worsen the complexity of the analysis problem, while making it easier to verify programs in practice. For example, proving termination of the simply-typed lambda calculus with natural numbers requires induction up to $\epsilon_0$, but by adding type polymorphism you get System F, whose termination proof as strong as the consistency of second-order arithmetic. Yet, in practice programs written in F are much easier to verify, because the modularity properties of second-order quantification make writing structured programs and correctness proofs much easier.