In short, if we prove $P=NP$, then we know a whole lot more about computation than we did before, even if we don't find the algorithm, and that was the objective behind research on $P=NP$ all along.
It's much worse, because most researchers believe that $P\ne NP$, meaning that even when the proof is discovered, it means that we won't be able to find a polynomial-time algorithm for SAT, not because we're looking in the wrong places, but because no such algorithm exists.
But that doesn't worry most complexity theorists, because the would-be algorithm for SAT that you describe is only a practical application, a spin-off, of the proof. And if you care about practical applications, then why are you working on $P=NP$? It's the most theoretical question in computer science!
Rather, the motivation behind research in this direction is* to better understand computation, very much akin to why mathematicians care about the Riemann hypothesis, and why physicists build giant particle colliders, even though we already have giant databases of prime numbers and even though the discovery of new particles mostly does not help us build faster rockets or better fusion reactors.
But what don't we understand about computation? We can build marvellous AI systems that recognize faces and Chinese characters, and predict the weather! Those are results of the form, this problem can be solved with so-and-so many resources, but on the flip side, one can ask, for this problem, what is the minimum amount of resources needed? The current state of affairs in the last regard is rather embaressing, because as far as we know:
- SAT has a linear-time (!) algorithm**
- SAT has an algorithm that uses $O(n^{1.802})$ time and $O(\sqrt{n})$ space
- every language in $NP$ has a circuit with $5n$ gates.
- The Succinct Circuit Satisfiability problem***, which is $NEXP$-Complete ($NEXP$ is the exponential-time version of $NP$), can be solved in polynomial time with a randomized algorithm with bounded error (i.e. it gives the wrong answer only with probability $\leq \frac{1}{n}$)
- Everything that can be computed using a polynomial amount of memory can be solved using a polynomial amount of time. For example, the Quantified Boolean Formula problem, which is like SAT except instead of an $\exists$ quantifier, there are any number of $\exists x\colon\forall y\colon\exists z\colon\cdots$ quantifiers.
Until these ridiculous scenarios are ruled out, we cannot honestly say that we understand computation in any depth. And that is the utility that you ask for, of why anybody at all works on $P=NP$.
I encourage you to read this wonderful survey of Scott Aaronson where in section 1.2 he addresses all the usual objections, like, what if $P=NP$ but we can't find the algorithm, or what if we do, but it's exponent is hopeless, or...
*as far as I can tell, as someone who is not a professional complexity theorist, but who did write his Master's thesis on the topic.
** We do not know whether nondeterminism gives you an advantage for solving SAT, but we do know, since 1983 [1] that nondeterminism gives you an advantage for some language, because there is a language $L$ solvable by a non-deterministic machine in $O(n)$ time but not by any deterministic machine in $O(n)$ time. In 2001, that result was improved [2] to a language in $NTime(n)$ but not in $DTime(n\sqrt{\log(n)})$.
*** The Succinct Circuit Satisfiability problem is this: fix some encoding of Boolean circuits as binary strings. You are given a circuit on $n$ inputs. Interpret the truth table of this circuit as a binary string of length $2^n$. Interpret that string as representing a circuit. Is that circuit satisfiable?
[1] Paul, Wolfgang J., et al. "On determinism versus non-determinism and related problems." Foundations of Computer Science, 1983., 24th Annual Symposium on. IEEE, 1983.
[2] Santhanam, Rahul. "On separators, segregators and time versus space." Computational Complexity, 16th Annual IEEE Conference on, 2001.. IEEE, 2001.