The difference between $\beta$-reduction and $let$

These are the reduction rules associated with $\beta$ reduction and $let$:

$$(\lambda x. e_2) e_1 \to_{\beta} e_2 [e_1 / x]$$
$$let \,x = e_1 \textit{ in }e_2 \to e_2 [e_1/x]$$

These reduction rules are very similar.

What is the point of having $let$ as well as $\beta$-reduction?

I can't see why it is of any use.

In the untyped lambda calculus, $\mathsf{let}$ is indeed useless, and most presentations leave it out. But in many typed lambda calculi, $\mathsf{let}$ is useful because it has a more general typing rule.

The best known example is the Hindley-Milner type system, which derives its power from let-polymorphism. In $(\lambda x.e_1) \: e_2$, the expression $e_1$ has one particular type, which is also the type of $x$ when typing $e_1$. But in $\mathsf{let} \: x = e_1 \: \mathsf{in} \: e_2$, $e_1$ can be polymorphic, and the instances of $x$ in $e_1$ can have different specializations of this polymorphic type.

StackExchange Computer Science Q#132015, answer score: 3