Are there any Zero-Knowledge Proofs?

I speculated before about zero-knowledge proofs and existentials. What I had in mind was encoding knowledge hiding via types. I suspect this result would be more interesting than I had imagined. Here is my understanding:

Zero-knowledge proofs are interactive proofs, and are therefore in the class IP. This class is the same as PSPACE, which is not yet known to be distinct from P (though it certainly contains P). So, it's possible that P = IP = PSPACE, and ZK proofs can't hide anything the verifier couldn't calculate herself. In other words, we may one day discover that most of our ZK proof protocols are useless. (This is not the whole story, as there are lots of variations on interactive proving.)

So, if there were a correspondence between these ZK proofs and existential types, it would either settle the P = PSPACE problem or discover a problem in type theory that is equivalent to it.

Each of these seems quite unlikely to me.

There is at least one person, however, who is doing research about the relationship between types and cryptography.