Why algorithms calculating non-tirivial zeros can't be used as proofs of Riemann Hypothesis?

Question

Recently I was reading again this propositions as types paper by Philip Wadler:

http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf

It gives an impression, that programs are proofs. So my first question was that why they are not enough for mathematical proofs then, for example in case of Riemann Hypothesis. Billions of zeros on critical line have been calculated in many many ways. I suppose they use some sophisticated algorithms or computer programs in that sense.

http://mathworld.wolfram.com/pdf/posters/Zeta.pdf

So, I was just stuck there. Why aren't these programs, or proofs in the system of Curry–Howard correspondence, enought?