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.
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?