Criteria for "constructive" in this question: Given a formal system and all the models that satisfy the axiomatic systems of interest (e.g. all models of ZF without choice), any object being constructed can be proved to exist/not exist and the proof is written only in terms of the sequence of axioms (and theorems derived from them) being used, and rejecting the law of excluded middle.
In ZF set theory where axiom of choice is absent, it is consistent that there exists amorphous and infinite dedekind finite sets, although we cannot prove them because we can construct models where they exist and models where they don't.
$S$ is infinite dedekind finite, or strictly dedekind finite if it does not biject with any initial section of the naturals (not of finite cardinality) and there exists no map that can inject $S$ into any of its subsets.
In particular, it is consistent that there can exist infinite dedekind finite subsets $S$ of the reals.
After discussing in the chat, it was found that $S \subsetneq \Bbb{R\setminus Q}$ and that $S$ consists of both a countable subset and another infinite dedekind finite set.
But that raised a question: It is known that any irrational $r$ is a rational distance away from some other irrationals $s$, therefore this will mean for any subset of irrationals, there always exists a nonzero rational $q$, not necessary unique, such that $s=r+q$ for any pairs of $r,s \in S$. Since $\Bbb{Q}$ is countable regardless of choice, it seems $\{s : s=r+q\}$ will always form a countable subset for any candidate $S$, thus leading to the conclusion that there cannot be any such $S$.
What is an explicit example of an infinite dedekind finite subset of the reals in models of ZF where they can be proved to exist. More generally, what well known models of ZF will allow the existence of such sets be provable and also constructible explcitly via an algorithm or procedure?
How to show that objects defined using both axiom of choice or its negation can never be constructive, is there a well known reference for such proof?
As far as constructivity, Arnie Miller has a proof that it is consistent to have a Borel set which is [infinite] Dedekind-finite.
In fact this Borel set is relatively low in the hierarchy, it is an $F_{\sigma\delta}$ set.
As far as "constructive", I guess this is more or less the best you can get. In the same paper he shows that it's impossible to get it from a lower stage of the Borel hierarchy.
If this answer does not satisfy you, then I'm afraid that there isn't much more we can say. Let me explain why by answering the second answer.
Suppose that $\varphi(x)$ is some formula which defines a set. And now you want to ask if the set it defines is provably such and such. For example, is it provably a finite set of ordinals, or provably a set of reals (for some canonical coding of the reals into sets).
Some formulas define things like that. Like the set of rational numbers, or the set of reals which are constructible in Gödel's sense.
But now we run into independence. In some models, we can show that no formula defines a Dedekind-finite set (or some other set whose existence defies the axiom of choice). Simply because in those models the axiom of choice holds, or sufficient fragment of it holds. And in some models we can prove that a certain set with a certain property does in fact exist.
This means that it is impossible, without the axiom of choice, to prove or disprove that $\varphi(x)$ defines a set with a certain property.
And it can get worse. Just assuming the failure of the axiom of choice, we can prove that Zorn's lemma fails. But we cannot point at a specific example, since the axiom of choice consistently holds up to some rank in the universe, and only fails very high. So anything you might want to define and prove that it "has to be a counterexample to Zorn's lemma" is going to fail.
In other words, the definitions "$\alpha$ is the least such that $V_\alpha$ is not well-orderable" and "$\alpha$ is the least ordinal such that $\mathcal P(\alpha)$ is not well-orderable" might be such that just assuming choice fails ensures that this $\alpha$ exists; but there is no algorithm for finding it, because we can always find models where choice fails above this $\alpha$. And the same is true for many other definitions of this sort.