(5/6) The new technology which allows us to construct this explicit counterexample is stateful realizability. There are several precursors and then also several more recent developments, but I'm referring to this 2019 breakthrough by Liron Cohen, Sofia Abreu Faro and Ross Tate: https://www.coalg.org/calco-mfps-2019/files/2019/05/mfps19-cohen-abreu_faro-tate.pdf

The paper invests some effort to explain that, in hindsight, the basic idea is simple. (But there are quite a few knobs, and for everything to work, they all need to be aligned. I guess I am far from the only one who briefly entertained something like this, but then, unlike them, failed to actually make it work.)

Recall the BKH interpretation of intuitionistic logic, giving newcomers a useful guiding principle of what constructive mathematics is about.

"A witness of 𝑃 ⇒ 𝑄 is a construction which converts witnesses of 𝑃 into witnesses of 𝑄."

"A witness of ∀𝑥 ∈ ℕ. 𝑃(𝑥) is a construction which converts numbers 𝑥 into witnesses of 𝑃(𝑥)."

And so on.

This is all very nice, but what exactly is a "construction"? For instance, if by "construction" we mean "function", then the full axiom of choice is trivially witnessed.

Original Kleene-style number realizability instead concretizes "construction" as "Turing machine", and says "realizer" instead of "witness": A machine 𝑒 realizes 𝑃, denoted 𝑒 ⊩ 𝑃, iff... (We then have that the axiom of choice, ∀𝑥∈𝐴. ∃𝑦∈𝐵. 𝑅(𝑥,𝑦) ⇒ ∃𝑓:𝐴→B. ∀𝑥∈𝐴. 𝑅(𝑥,𝑓(𝑥)), holds for all those 𝐴 for which we can compute canonical representatives, for instance 𝐴 = ℕ but not 𝐴 = ℕ^ℕ.)

Now stateful realizability concretizes "construction" as "machine which (may be nondeterministic and) has access to (some form of) persistent memory". A machine 𝑒 realizes 𝑃 in state 𝑠, denoted 𝑠 | 𝑒 ⊩ 𝑃 iff...