Its the program itself that is the proof, not the computer running the program.
In a sufficiently powerful type system you can express any proposition as a function type. A proof of that proposition is also a program. The proof checker is a type checker. If your proof is invalid, your program won't type-check.
But what if the program that runs the proof will never terminate? For example I could write a 'proof' for some property of natural numbers by just iterating through all of them and every time validating the property.
Isn't a proof only valid if it can be validated within a reasonable amount of time, either by some human or by a computer?
Quoting from Wikipedia:
"Because of the possibility of writing non-terminating programs, Turing-complete models of computation (such as languages with arbitrary recursive functions) must be interpreted with care, as naive application of the correspondence leads to an inconsistent logic. The best way of dealing with arbitrary computation from a logical point of view is still an actively debated research question, but one popular approach is based on using monads to segregate provably terminating from potentially non-terminating code (an approach that also generalizes to much richer models of computation,[6] and is itself related to modal logic by a natural extension of the Curry–Howard isomorphism[ext 1]). A more radical approach, advocated by total functional programming, is to eliminate unrestricted recursion (and forgo Turing completeness, although still retaining high computational complexity), using more controlled corecursion wherever non-terminating behavior is actually desired."
That is not what programs as proofs means. It is not that the program finds or performs the proof; the program is the proof, in a certain formal sense. The thing it proves is its type. The validation step is type-checking. For most programming languages, type-checking is decidable, so testing whether the proof is valid is fine. However, most programming languages correspond to trivial proof systems (every type is inhabitable, so every proposition is provable).
This is part of the problem with proofs-as-programs: it's a beautiful theory, and inspires a lot of useful work, but if taken too literally it's wrong and useless.
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.
In a sufficiently powerful type system you can express any proposition as a function type. A proof of that proposition is also a program. The proof checker is a type checker. If your proof is invalid, your program won't type-check.
Coq (https://coq.inria.fr/) is a real-world example of exactly this.