Can we disallow finite choice?

You might want topos theory. A topos is something like the category of sets, but the internal logic of a general topos is much weaker than ZF; it need not even be Boolean. An example of a topos is the category of sheaves of sets on a topological space. You can use topos theory to turn voodoo-sounding statements of constructive mathematics into ordinary mathematical statements which you can understand: for example "a nonempty set S might not have any elements" becomes "a sheaf S which is not the empty sheaf might not have any global sections" (or possibly "might not have local sections everywhere"), which is of course true. A canonical reference on this subject is Mac Lane & Moerdijk, Sheaves in Geometry and Logic.

This is possible in constructive mathematics, because it distinguishes between finite sets and sets with a counted number of elements. (I'm not quite sure what the standard terminology is, though.)

A set $S$ is finite if there is a natural number $n$, such that there is a surjective map from $[0, \ldots, n-1]$ to $S$. A set $T$ is counted, if there is an $m$ such that there is an isomorphism between it and the numbers $[0, \ldots, m-1]$.

Now, note that finiteness bounds the number of elements in $S$ -- there can be no more than $n$. However, we do not necessarily know exactly how many elements there are, since equality may not be decidable on $S$. (That is, we might not know how to show for every $s$ and $s'$ that $s = s'$ or $s \not= s'$.) Of course, countedness implies finiteness (just take one half of the iso). It also implies decidable equality on the elements (since we can convert two $T$s to natural numbers, and compare those). Likewise, finiteness and decidable equality imply countedness (iterate over the elements of $S$, and use equality to identify the duplicates). But finiteness alone is not sufficient to imply countedness.

This seems to me to capture the intuition that we might not always have the distinguished isomorphism available. A combinatoric argument gives a method for (constructive) counted sets. One that doesn't use choice gives a method which will also work (constructive) finite sets.

Actaully, you can avoid such arcane horrors as categories and topoi. When moving from infinite to finite, much of the difficulty (imo) is in figuring out 1) how the original statement was really algorithmic in nature and 2) what the implicit resource bounds were. Once you figure these statements out, it becomes much clearer what the AC-oracle is actually doing for the algorithm, and then come up with analogous resource bounds.

My sense is that approaching your problem(s) this way will be both more useful and satisfying that assuming that some battery of huge guns is going to work one day.

For specific references, you might look at the work of Blass, Gurevich and Shelah on "Choiceless Polynomial Time" -- this is essentially computing using the hereditarily finite sets over a finite set of atoms. The finite-model theory literature is full of work on the power of various models of computation with and without a linear order. There is also a (largely incomprehensible, but what can you do) paper of Shelah's on classifying second-order quantifiers over finite universes.