Lambda calculus outside functional programming?
You are asking for an application outside of computer science and logic. That is easily found, for example in algebraic topology it is convenient to have a cartesian closed category of spaces, see convenient category of  topological spaces on nLab. The formal language corresponding to cartesian closed categories is precisely the $\lambda$-calculus. Let me illustrate with a very simple example how this comes in handy.

First, as a warmup exercise, suppose someone asks you whether the function $f : \mathbb{R} \to \mathbb{R}$ defined by $f(x) = x^2 e^x + \log (1 + x^2)$ is differentiable. You do not actually have to prove that it is, you just observe that it is a composition of differentiable functions, therefore differentiable. In other words, you made an easy conclusion based on the form of definition.

Now for the real example. Suppose someone asks you whether the function $f : \mathbb{R} \to \mathbb{R}$ defined by
$$f(x) = \left(\lambda f : \mathcal{C}(\mathbb{R}) . \int_{-x}^{x} f(1 + t^2) dt\right)(\lambda y : \mathbb{R} . \max(x, \sin(y + 3))$$
is continuous. Again, we can immediately answer "yes" because the function is defined using the $\lambda$-calculus and starting from continuous maps $\max$, $\int$, $\sin$, etc.

Various extensions of the $\lambda$-calculus make it possible to do the same sort of thing in other areas. For example, because a smooth topos is a cartesian closed category, any map which is defined using the $\lambda$-calculus, starting from derivatives and the ring structure of the reals (and you can throw in the exponential function if you wish) is automatically smooth. (Actually, the main thrust of the smooth topos is the existence of nilpotent infinitesimals which allow you to meaningfully say things like "we disect a disc into infinitely thin isosceles triangles".)