As others have observed before, you cannot simply say "computable" and "ZF" in the same sentence without explaining what you mean. But I can tell you what your options are.

In order to speak about computability you have to provide some sort of an axiomatization or a model of computability. ZF is not such a model, but there are many others. Let us look at some of them and what happens to the axiom of choice. In what follows I mean by "computable model" a model of set theory or type theory in which all (global) maps are computable in some sense. In particular, choice functions happen to be computable in such models, so far as they exist.

**Intuitionistic set theory IZF** is an intuitionistic variant of set theory. It has many different models, some of which are computable. In IZF we can prove that the axiom of choice implies the law of excluded middle, so this kind of destroys the I in IZF. But restricted forms of choice are ok, notably countable and dependent choice are fine (in the sense that they are consistent with IZF and are validated by various computable models of IZF).

**Higher-order intuitionistic logic (internal language of a topos)** is essentially the same as IZF with regards to choice.

**Martin-Löf type theory** is a formulation of constructive mathematics in which choice is valid, in fact it is easy to prove it. The caveat here is that the interpretation of logic is a bit unusual because a proposition is equated with the collection of its proofs (as opposed to with its extension).

**Brouwerian intuitionism** accepts some choice but not all. More precisely, it accepts countable choice and $AC_{1,0}$, which is choice for families indexed by the set $\mathbb{N}^\mathbb{N}$. There are computable models of Brouwerian intuitionism (certain kinds of realizability models).

**Bishop-style constructive mathematics** accepts countable and dependent choice but not more. It has many computable and classical models because it is agnostic with respect to the law of excluded middle.

**Russian constructivsm** is another form of constructivism which accepts countable and dependent choice, but not more. The effective topos is a model.

**Realizability toposes** provide a rich class of models of computability. In fact, they are so general that the topos of (classical) sets is a special case. I should also point out that realizability toposes are *larger* than classical sets because they contain the category of sets as a subtopos of sheaves (for the double negation topology). Therefore, they provide the sort of setup that is needed to make sense of your question. In those realizbility toposes that are built from reasonable computational models, i.e., those that are based on the standard notion of Turing computability, choice is never generally valid. This is so because general choice implies the law of excluded middle (as mentioned above), and the law of excluded middle allows us to define the Halting oracle. Nevertheless, countable choice is always valid, which is one reason why various "schools of computability" accept it. In some realizability toposes you get more choice, but never a lot.

Let me make one last remark. There is a very general principle that "computable maps are continuous", where of course we have to look at "correct" topologies for this to make sense. (Ask a MO question if you want to know why.) Applied to choice this says that computable choice functions are continuous. But it is quite easy to come up with examples where the choice function cannot be continuous, for example we cannot choose continuously for each $x \in \mathbb{R}$ an integer $k \in \mathbb{Z}$ such that $x < k$. So you need not get into computability to see why choice has to fail in certain contexts. This might be helpful if you are familiar with topological sheaves.

`$\{A_r : r \subseteq \omega\}$`

where `$A_r = \{ x \subseteq \omega : r <_T x \}$? $\endgroup$ – François G. Dorais♦ May 23 '10 at 15:51canbe proved constructively. Just have a look at Bishop's "Foundations of Constructive Analysis". You will find the intermediate theorem there, too. $\endgroup$ – Andrej Bauer May 24 '10 at 12:40