One of the characteristics of many constructive theories is that they have the "term existence property": if a statement $(\exists x)\phi(x)$ is provable, then there is a term $t$ such that $\phi(t)$ is provable. Moreover, usually $t$ can be extracted algorithmically from a formal proof of $(\exists x)\phi(x)$.
The term existence property is exactly a rigorous way to say that, if an existential statement is provable, then it is possible to explicitly describe a witness. Many constructive theories have this property or restricted version of it. The restriction to the case where the $(\exists x)$ quantifies over natural numbers is usually of particular interest.
The current version of the wikipedia article has some useful information and references.