What about programs that, by design, run indefinitely and do useful things? Say, a server that just responds to requests as they come. Is that "not a real program" for purposes of CH?
Or what about ones with side effects?
It seems to assume away a lot of (what is called) programs in actual practice.
There are accounts of infinitely-running programs as proofs; they have to do with the proof technique of conduction, which has to do with proving properties of infinite data structures; a counterpart of the more familiar technique of induction, which lets you prove things about finite data structures.
Side effects are a little harder to see proof-theoretically; for some effects there are reasonable stories (exceptions, for example, are a special case of continuations, which have connections to classical logic), but for many I think the story is still murky.
The Curry-Howard correspondence is more of a lens through which to approach PL theory, or an evolving research agenda, than it is a settled account of all programming practice.
As long as there is any structure or internal logic to what the program does, it can be reflected in its types.
For your example of a server, look at the Servant library in haskell. It allows you to define type safe routes and links, ensuring that your program exactly matches the API, and that no links are ever broken.
Or what about ones with side effects?
It seems to assume away a lot of (what is called) programs in actual practice.