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.

Existentials and Zero-Knowledge Proofs

When I use "∃ x . P(x)" in typed programming (using intuitionistic logic), I must have in hand an x and a proof of P(x). This is not the case in the classical logic, in which I might have a proof of ∃ x . P(x) without knowing any details of x at all.

This idea that I know such an x exists though I have no knowledge of it reminds me of zero-knowledge proofs. Of course, the zero-knowledge proofs referenced in the Wikipedia article aren't so much proofs as they are assurances with high probability. I looked around for zero-knowledge proofs that were more proof-like, but I didn't find much. I wonder if there is any deeper connection between classical existentials and zero-knowledge proofs?