Tightening application rules for STLC
Shouldn't the application rule be written:
$(\lambda x : \tau . e \space e : \tau)$ ?

No, there are at least three problems with this formulation:

First, it is important that the first time can be a variable. For example, we want to allow the term
$$
x \; y
$$
Why do we want to allow this? Well we want to be able to apply a function to an argument. For example, the following lambda term is a function which applies $x$ to $y$:
$$
\lambda x: \tau_1 \to \tau_2. \lambda y: \tau_1. (x \; y)
$$

Second you are assuming the first term has already been reduced. This is not generally true. Although once reduced, the term $e_1$ in $(e_1 \; e_2)$ should usually be a lambda expression (or a variable), this may not hold before it has been evaluated.

The third problem is really a misunderstanding, not a concrete issue with your formulation: in STLC, we allow terms that are not well-typed. For example, if there are base types including numbers and Booleans, then we can write nonsense like
$$
\text{true} \; 3
$$
and this is a valid lambda term, just not a well-typed one. So your question seems to want to make sure that the application rules is well-typed, but that will be part of the typing rules, not part of the definition of a lambda term itself.



The only time an application makes sense both intuitively and type-wise is by reducing and abstraction by replacing its variable with an expression.

That is correct, and this is going to be the motivation for the typing rules. In fact, the typing rule will say this exactly: the term $e_1 \; e_2$ will be well-typed only if $e_1$ is a function $\tau_1 \to \tau_2$ and $e_2$ is a value of type $\tau_1$. But for the reasons above, it is important that these restrictions be on the typing level, not baked into the syntax.

$(x \space e)$ makes no sense.

It does make sense: but only in a context where $x$ is a variable of a function type. Think of a variable that may be assigned to a value; if it is assigned to a value which is a function, then this makes sense.

$(c \space e)$ again, you can't apply to a value.

It's true that this makes no sense, but we allow it anyway; we just don't say that it is well-typed.

$((e \space e) \space e)$

As you said this case may resolve to one of the other cases, but we are defining the syntax here, not the semantics. So it doesn't imply that we should rule it out just because resolves to the other cases; it is still a valid lambda term, just one that is not fully reduced.