EDIT: This post was substantially modified with the help of the comments and answers. Thank you!
Judging by their definitions, the $\mathrm{Ext}$ and $\mathrm{Tor}$ functors are among the most non-constructive things considered in algebra:
(1) Their very definition requires taking an infinite projective or injective resolution; constructing a homotopy equivalence between two such resolutions requires infinitely many choices.
(2) Injective resolutions are rather problematic in a constructive world (e. g. the proof of "injective = divisible" requires Zorn, and as far as I understand the construction of an injective resolution relies on this fact).
(3) Projective/injective resolutions are not really canonical, so $\mathrm{Ext}$ and $\mathrm{Tor}$ are not functors from "pairs of modules" to "groups", but rather functors from "pairs of modules" to some category between "groups" and "isomorphism classes of groups". This is a problem already from the classical viewpoint.
(4) Projective resolutions are not guaranteed to exist in a constructive world, because the free module on a set needs not be projective! In order to avert this kind of trouble, we could try restricting ourselves to very well-behaved modules (such as, finite-dimensional over a field), but even then we are in for a bad surprise: Sometimes, the "best" projective resolution for a finitely-generated module uses non-finitely-generated projective modules (I will show such an example further below). These can be tricky to deal with, constructively. Mike Shulman has mentioned (in the comments) that injective and projective resolutions (and already the proofs that the different definitions of "projective" are equivalent, and that the different definitions of "injective" are equivalent) require choice – maybe the currently accepted notions of injectivity and projectivity are not "the right one" except for finitely-generated modules? (Cf. also this here.)
On the other hand, if we think about the ideas behind $\mathrm{Ext}$ and $\mathrm{Tor}$ and projective resolutions (I honestly don't know the ideas behind injective resolutions, besides to dualize the notion of projective resolutions), they are (at least partially) inspired by some of the most down-to-earth constructive mathematics, namely syzygy theory. So a natural question to pose is: How can we implement the theory of $\mathrm{Ext}$ and $\mathrm{Tor}$, or at least a part of this theory which still has the same applications as the whole theory, without having to extend our logical framework beyound constructivism?
It is not hard to address the issues (1), (2), (3) above one at a time, at least when it comes to the basic properties of $\mathrm{Ext}$ and $\mathrm{Tor}$:
For (1), the workaround is easy: If you want $\mathrm{Ext}^n\left(M,N\right)$ for two modules $M$ and $N$ and some $n\in\mathbb N$, you don't need a whole infinite projective resolution $…\to P^2\to P^1\to P^0\to M$. It is enough to have an exact sequence $P^{n+1}\to P^n\to P^{n-1}\to …\to P^1\to P^0\to M$, where $P^0$, $P^1$, …, $P^n$ are projective. (It is not necessary for $P^{n+1}$ to be projective. Generally, $P^{n+1}$ is somewhat like a red herring when $\mathrm{Ext}^n\left(M,N\right)$ is concerned.)
For (2), the only solution I know is not to use injective resolutions. Usually, things that can be formulated with projective resolutions only can also be proven with projective resolutions only. But this is not a solution I like, since it breaks symmetry.
(3) I think this is what anafunctors are for, but I have not brought myself to read the ncatlab article yet. I know, laziness is an issue… At the moment, I am solving this issue in a low-level way: Never speak of $\mathrm{Ext}\left(M,N\right)$, but rather speak of $\mathrm{Ext}\left(M_P,N\right)$ or $\mathrm{Ext}\left(M,N_Q\right)$, where $P$ and $Q$ are respective projective/injective resolutions. This seems to be the honest way to do work with $\mathrm{Ext}$'s anyway, because once you start proving things, these resolutions suddenly do matter, and you find yourself confused (well… I find myself confused) if you suppress them in the notation. [Note: If you want to read Makkai's lectures on anafunctors and you are tired of the Ghostview error messages, remove the "EPSF-1.2" part of the first line of each of the PS files.]
Now, (4) is my main problem. I could live without injective resolutions, without the fake canonicity of $\mathrm{Ext}$ and $\mathrm{Tor}$, and without infinite projective resolutions, but if I am to do homological algebra, I can hardly dispense with finite-length projective resolutions! Unfortunately, as I said, in constructive mathematics, there is no guarantee that a module has a projective resolution at all. The standard way to construct a projective resolution for an $R$-module $M$ begins by taking the free module $R\left[M\right]$ on $M$-as-a-set – or, let me rather say, $M$-as-a-type. Is this free module projective, constructively? This depends on what we know about $M$-as-a-type. Alas, in general, modules considered in algebra often have neither an obvious set of generators nor an a-priori algorithm for membership testing; they can be as complicated as "the module of all $A$-equivariant maps from $V$ to $W$" with $A$, $V$, $W$ being infinite-dimensional. Some are even proper classes, even in the classical sense. The free module over a discrete finite set is projective constructively, but the free module over an arbitrary type does so only if we allow a weaker form of AC through the backdoor. Anyway, even if there is a projective resolution, it cannot really be used for explicit computations if the modules involved are not finitely generated. Now, here is an example of where non-finitely generated modules have an appearance:
Theorem. If $R$ is a ring, then the global homological dimension of the polynomial ring $R\left[x\right]$ is $\leq$ the global homological dimension of $R$ plus $1$.
I am referring to the proof given in Crawley-Boevey's lecture notes. (Look at page 31, absatz (2).) For the proof, we let $M$ be an $R\left[x\right]$-module, and we take the projective resolution
$0 \to R\left[x\right] \otimes_R M \to R\left[x\right] \otimes_R M \to M \to 0$,
where the second arrow sends $p\otimes m$ to $px\otimes m-p\otimes xm$, and the third arrow sends $q\otimes n$ to $qn$. (This is a particular case of the standard resolution of a representation of a quiver, which appears on page 7 of a different set of lecture notes by the same Crawley-Boevey.)
Now, the problem is that even if $M$ is finitely generated as an $R\left[x\right]$-module, $R\left[x\right] \otimes_R M$ needs not be.
Is there a known way around this?
Generally, what is known about constructive $\mathrm{Ext}$/$\mathrm{Tor}$ theory? Are there texts on it, just as Lombardi's one on various other parts of algebra (strangely, this text talks a lot about projective modules, but gives $\mathrm{Ext}$ and $\mathrm{Tor}$ a wide berth)? Do the problems dissolve if I really use anafunctors? Do derived categories help? Should we replace our notions of "injective" and "projective" by better ones? Or is there some deeper reason for the non-constructivity, i. e. is $\mathrm{Ext}$/$\mathrm{Tor}$ theory too strong?
Endnote for everyone who does not care about constructive mathematics: Even dropping constructivism aside, I believe that there remain quite a lot of real issues with homological algebra. First there is the matter of canonicity, then there is the problem of too-big constructions (proper classes etc.), the frightening unapproachability of injective covers, the idea that one day we might want to work in a topos where even ZF is too much asked, etc. I am changing the topic to a discussion of how to fix these issues (well, it already is such a discussion), constructivism being just one of the many directions to work in.
Best Answer
I have some sympathy for the question, since I have gotten bothered by the noncanoncity -- although less so by the nonconstructivity -- of the usual definition in my youth. (These days I'm less bothered by such things.) Here are a few ways around it for $Ext$.
There is a definition going back Yoneda, I think, of $Ext^n(M,N)$ as an equivalence class of exact sequences $0\to N\to \ldots \to M\to 0$ of length $n+2$ (including $M,N$). Take a look at Hilton and Stammbach's Homological Algebra. This is quite cumbersome but it solves the dependency on, let alone existence of, suitable resolutions.
This was mentioned already by Mike Shulman. You can take $Ext^n(M,N)= Hom_{D(R)}(M,N[n])$ in the derived category $D(R)$ of $R$-modules. Once you get used to the formalism, this is much more convenient than 1 (at least for me).
Addendum Regarding your original question about how constructive this can be made, I think for certain classes of modules (e.g. finitely presented modules) over certain classes of rings (e.g. polynomial rings), this is not only possible, but it seems to have been implemented in some computer algebra packages already. I notice that the latest Macaulay 2 has commands for Ext and Tor.
*If your are unhappy with this, use instead the double character module $$I(N)= Hom_{\mathbb{Z}}(Hom_{\mathbb{Z}}(N,\mathbb{Q}/\mathbb{Z}), \mathbb{Q}/\mathbb{Z})$$