Let me summarize what I think I understand about constructivism:
"Constructive mathematics" is generally understood to mean a variety of theories formulated in intuitionist logic (i.e., not assuming the law of excluded middle, $\neg\neg A\Rightarrow A$ (LEM)) so that, broadly speaking, in order to prove $A \lor B$ one must prove either $A$ or $B$ ("disjunction property") and, in order to prove $\exists x.A(x)$ one must "construct" some $x$ and prove $A(x)$ for it ("existential property"). There are a number of systems of constructive mathematics, and variations on the requirements (I don't claim to know the details), but, as far as I understand it, all of them operate in the absence of the LEM which is considered one of, if not "the", root cause of non-constructivism. So constructive mathematics in this sense represents a fairly radical departure from classical mathematics, as the abandonment of the LEM represents a considerable break from accustomed practice; the upside, of course, is that a constructive proof will provide some benefits that a classical proof will not (e.g., extracting algorithms from proofs or something of the sort).
(I hope I didn't write too much nonsense here. Onward to $\mathsf{ZF}$.)
On the other hand, consider $\mathsf{ZF}$, i.e. Zermelo-Fraenkel set theory without the axiom of choice, formulated in classical logic. This also represents a departure from the more habitual $\mathsf{ZFC}$, although not as radical as the abandonment of the LEM. Some of the differences (with classical $\mathsf{ZFC}$), however, are vaguely of the same flavour: e.g., in (some varieties of) constructive mathematics one cannot prove the existence of discontinuous real functions, while in $\mathsf{ZF}$ one cannot prove the existence of non-measurable real functions; in constructive mathematics, the powerset of a finite set might fail to be finite, while in $\mathsf{ZF}$ the powerset of a well-orderable set might fail to be well-orderable; in both cases, one need be careful about what "finite" means (although the subtleties are considerable greater in constructive mathematics as in $\mathsf{ZF}$). This leads me to wonder whether there is a pattern of similarity.
Very often, we ("we" being classical mathematicians) say that we cannot exhibit some object because its construction requires the axiom of choice: e.g., I cannot exhibit a basis of $\mathbb{R}$ as a $\mathbb{Q}$-vector space or a non-principal ultrafilter on $\mathbb{N}$ or this kind of things.
But conversely, we will say that we can exhibit a bijection between $X$ and $Y$ given injections $X\to Y$ and $Y\to X$, because the proof of the Schröder-Bernstein theorem does not use the axiom of choice (even though it is probably not constructive); and, while hardline constructive mathematicians will disagree, I think most classical mathematicians will agree that it does, indeed, "construct" a bijection. Similarly, this paper, which shows in $\mathsf{ZF}$ that if there is a bijection between $n\times X$ and $n\times Y$ (where $n$ is a natural number) then there is one between $X$ and $Y$ does it by "exhibiting" a kind of algorithm which it claims is somehow canonical ("pan galactic division"). This is all reminiscent of the ideas of constructivism, even though it is not fully constructive.
(This is far too long, but I feel it is necessary to illustrate where I'm getting at.)
All of the above leads me to ask whether the similarity/analogy between $\mathsf{ZF}$ and constructive mathematics can be made precise. Or, a little less vaguely:
Question(s): Is there some well-defined sense in which $\mathsf{ZF}$ (in classical logic, but as opposed to $\mathsf{ZFC}$) can be said to be "somewhat constructive"? E.g., does it satisfy some very weak version of the existential property? Can we formalize the intuitive idea that proving the existence of an object in the absence of Choice "exhibits" the object in a stronger sense than proving its existence in $\mathsf{ZFC}$ (as the case of Schröder-Bernstein illustrates)?
A followup or related question might be whether there exist theories defined in classical logic that have an even stronger "constructive flavour" than $\mathsf{ZF}$, i.e., if the above question makes sense, that are "fairly constructive" without going all the way to abandoning the LEM.
Additional comments: One (to me) confusing fact is that constructive theories often incorporate some variant of the axiom of choice (see, e.g., here); the relation between these constructive axioms of choice and the axiom of choice from $\mathsf{ZFC}$ (which, as I explain above, seems to be anti-constructive) is unclear to me: so maybe I'm missing a big part of the picture. And at the other extreme, $V=L$, which seems to be a kind of super axiom of choice, makes it possible to "exhibit" some things which could not be exhibited without it, e.g., a well-ordering of $\mathbb{R}$ (or just about anything: take the $<_L$-least element such that <blah blah blah>).
