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?