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