Has the semantics of TeX (as a programming language) ever been formalized? It seems to me that the macro language employed by $\TeX$ can maybe be seen as some kind of term rewriting system or some kind of programming language with call-by-name scoping.

Even modern implementations of the $\TeX$ engine (e.g. $\mathit{Xe}\TeX$) interpret code in a quite direct way and I'm not aware of any attempt at optimizing the execution (like modern optimizing interpreters can do). However, devising correct optimization passes for a language like $\TeX$ is going to be very difficult because of the "action at a distance" that macro redefinitions can have, and the ability of redefining macros by calling them by name.

So implementing an hypothetical optimizing interpreter for $\TeX$ sounds a very difficult problem in practice but also a very useful one, since $\TeX$ is used all over math and science and slow compilation times are a known drawback of the system. Note that the majority of time is spent interpreting code, not computing the actual typesetting, especially when computationally heavy packages are used (such as tikz).

Maybe a formal semantics for the language could be a start to address the problem. So has the semantics of the $\TeX$ programming language ever been formalized?
No, to my knowledge there has been no work on formalizing TeX of the kind you are interested in.

(What follows is a subjective and personal commentary). I think it is an intriguing and well-posed idea, and your motivation of using it to perform optimizations sounds reasonable -- another related question is whether you could define a bytecode format for it to speed up interpretation. On the other hand, the idea has two downsides.

First, it is not clear to me that there is a large potential for optimizations (for example, what kind of program-preserving transformations could one perform to speed up computation?), as it may be that the language semantics is intimately related to parsing the character flow, and thus not very accommodating to the design of optimization-friendly intermediate representations.

Second, the need for improvements in TeX interpretation speed is not well-established: the speed of batch speed building has remained reasonable thanks to hardware improvements. Cases where speedups could be welcome are complex graphics package (beamer presentations can take quite some time to build), packages embedding rich computations (but then another language may be more appropriate), and use cases requiring fast rebuild for instant user feedback (but then incrementality, rather than optimization, may be the point; a formal semantics would certainly help reason about incremental implementations as well).

That is to say: this sounds like a fun, instructive topic, but it is not clear to me that the practical justifications for doing the work are strong. If someone was interested in doing it out of curiosity, that sounds like an excellent adventure, but otherwise there may be other ways to employ the same skillset whose impact would be more sought-after by end-users.