Nice question! I think that your notion of an "effectively computable reduction" is interesting and worth studying, but not as fundamental as standard reductions. Let me provide some observations about this notion that may be illuminating:
Observation 1: it does not make sense to talk about effectively computable reductions from one language to another; only from a family of languages to another.
In particular, you seem to be mixed up when you write this:
Most reductions for NP-hardness proofs I encountered are effective in the sense that given an instance of our hard problem, they give a polynomial time algorithm for our problem under question by using reductions. All reductions in the 21 classic problems considered by R. Karp work this way.
A reduction from, say, VertexCover to 3SAT is a Turing machine $f$ that transforms instances of VertexCover into instances of 3SAT. Since it is a Turing machine, it is effectively computable by definition. So it is not surprising that all reductions you have seen of this form are effectively computable.
In other words, if we just look at reductions from one language to another, then every reduction is effectively computable!
This is different from the case of the Cook-Levin theorem, where we have to show a reduction $f$ from an arbitrary NP language to SAT. Then it might make sense to consider whether this reduction -- parameterized by the language in NP -- is effective or not. But that brings us to my second point:
Observation 2: What counts as an effectively computable reduction depends on the representation of languages.
This is important because standard reductions (either many-to-one reductions or Turing reductions) do not depend on the way the language is represented. For a reduction from $L$ to $L'$, I consider $L$ and $L'$ to be subsets of $\{0, 1\}^*$. But for your notion of effectively computable to make sense, we need to have access to a representation of $L$ (we probably don't need a representation of $L'$).
To make this point clearer, consider the reduction in the proof of the Cook-Levin theorem, which you brought up. The proof considers a language $L$, represented by a polynomial-time nondeterministic Turing machine $N$. Then it shows that $L$ is reducible to SAT. You say that this reduction is not effectively computable, but that depends on how $N$ is represented, i.e., the definition of a polynomial-time nondeterminstic Turing machine $N$:
Definition 1: A polynomial-time NTM is a nondeterministic Turing machine such that there exists a polynomial $p(n)$, such that the TM always halts in time at most $p(n)$.
Definition 2: A polynomial-time NTM consists of a nondeterministic Turing machine, together with a polynomial $p(n)$. The way it runs is that, on any branch, it is only executed for $p(n)$ steps; if it does not halt in this time, then that branch is ignored.
It may seem that I am making Definition 2 up and that the definition is not natural, but actually both of these are perfectly valid definitions of a polynomial-time NTM that both have their merits. And for the classical theory of P, NP, and NP-completeness, both of these definitions are equivalent. The nice thing about Definition 2 is that an NTM is allowed to diverge on certain branches; you don't worry about that because the execution semantics says that we just forget about it once the running time goes above $p(n)$.
However, the definitions become inequivalent when it comes to effectively computable reductions. Note that, according to Definition 1, when we are given a language defined by an NTM $N$, we have no idea what its running time is, so we may not be able to reduce it to SAT (more on this below). But according to Definition 2, part of the NTM $N$ is that it comes with a polynomial, and so we know its running time. Therefore, we can effectively reduce all NP languages to SAT if we are using Definition 2.
Also, we have only considered nondeterministic Turing machines; we could equivalently define NP using verifier Turing machines. Then the definition of an effectively computable reduction could be something else!
TL;DR: Depending on how a language in NP is represented, and in particular depending on the definition of a polynomial-time NTM, it may be either true or false that every language in NP is effectively reducible to SAT. In other words, The set of effectively computable reductions changes depending on the model of computation used to represent languages in NP.
Now at this point, given points (1) and (2), a question still remains: can the reduction in the Cook-Levin theorem be made to be effective? In particular, suppose we fix the following definitions:
Languages in NP are represented by nondeterministic Turing machines whose runtime is bounded by an unknown polynomial $p$ (i.e. Definition 1).
Given a language $L$, we say that the class of languages NP is effectively poly-time reducible to $L$ if the following holds: there is a TM $f$ that takes as input $\langle N, w \rangle$, where $N$ is a polynomial-time NTM and $w$ is any input to $N$, such that $w \in L(N)$ if and only if $f(\langle N, w \rangle) \in L$. Also, $f$ must run in polynomial time (in its input $\langle N, w \rangle$).
In other words, to address point (1), we are assuming that languages in NP are represented by nondeterministic Turing machines without an explicit polynomial bound. And to address point (2), in our definition of effectively reducible, we are talking about a reduction from a class of languages, in this case NP, to a single language.
Now we have the following observation:
Observation 3: (Cook-Levin is not effective) The class NP is NOT effectively reducible to SAT.
Let us see why this is true. Assume towards a contradiction that an effective reduction $f$ exists. The idea is that we will try to solve a difficult (say, doubly-exponential-time) problem by taking its instance, turning it into a polynomial-time NTM, and asking $f$ to reduce it to SAT. So, let $L_{hard}$ be some problem that requires doubly-exponential time to solve (this exists by the Time Hierarchy theorem), and let $M_{hard}$ be a (deterministic) TM that solves it. Given any instance $w$ of the problem, define the following NTM $N_w$:
\begin{align*}
N_w :=
&\text{"On any input $a$, first run } M_{hard} \\
&\text{on input } w \text{. When it halts, accept if} \\
&\text{it accepts and reject if it rejects."}
\end{align*}
Now we can use this to solve $L_{hard}$ in exponential time (not double exponential), as follows. On input $w$, we first construct $N_w$, which has size only a constant more than $w$. Then we pass $\langle N_w, \epsilon \rangle$ (the second argument, $\epsilon$, is just a placeholder here) to $f$ to reduce it to SAT. $f$ gives us back an instance of SAT that is at most polynomial size in $N_w$, and $f$ takes only polynomial time to run. So we end up with an instance of SAT of polynomial size in $w$; now we solve it in exponential time in $w$ using brute-force search.
This point (3) seems to suggest that most of the time, no interesting class of languages will be reducible in this effectively computable sense to a single language. It will just be too hard, because you can exploit this computability to then solve hard problems by encoding them as part of a TM input to the effective reduction. However, something is a bit fishy here, because if we feed the TMs $N_w$ into the Cook-Levin theorem reduction, we would end up with very large SAT formulas, exponential in $w$. So perhaps our definition needs to be tweaked so that $f$ runs in time polynomial in the running time of $N_w$, not just polynomial in the input $\langle N_w, \epsilon \rangle$.
Observation 4: If we allow Turing (many to many) reductions, then Cook-Levin can be made effective.
As D.W. says in a comment:
I think one can construct an effective Cook reduction, by iterative doubling. Does that help?
I also believe this is true. In particular, we can change our definition of an "effective reduction" from NP to a language $L$ by saying that the reduction does not just return an instance of $L$, but returns many instances of $L$ in sequence, and uses an oracle for $L$ to solve the original problem. Then to solve a general problem in NP, you could try larger and larger polynomials $p$ until you get the right one which bounds the running time. You can detect whether a particular polynomial bounds the running time on all branches of the NTM by a separate reduction to SAT.
Disclaimer
I am not an expert in this topic. These are just some preliminary notes on the idea, and I am not sure if someone has studied this in the literature.
P.S. Although it may not be directly related, your question about considering effective reductions reminds me of an idea I had, about considering not just whether languages are in P or in NP, but whether they are provably so. This is related to the idea of developing a complexity theory that is effective or constructive. I asked and later answered question about defining provably P and provably NP languages here.
