You have to pay close attention what system of logic the proofs are written in. So, for example, it is an open problem, how and whether proofs written in homotopy type theory can be interpreted computationally (source: http://en.wikipedia.org/wiki/Homotopy_type_theory#Computer_p...).

I thought this was more or less solved with the recent developments on the cubical sets models? There is even a toy interpreter with univalence and higher inductives:

https://github.com/simhu/cubical

They've done a lot of good work, but it's not quite done yet. The original conjecture has not been answered in the affirmative, and there are also further questions...