I am not explaining how, I am merely pointing out that there is a "how to compute" question, and that lambda calculus and type theory help address that question

I am not explaining how, I am merely pointing out that there is a "how to compute" question, and that lambda calculus and type theory help address that question formally. That point tries to address the following question by OP: > What is the equivalent computer science problem that lambda calculus can help you solve? That may sound very obvious in retrospect - surely OP knew already what I was saying, and he actually wanted explanations on the how itself. Perhaps that's why it seems useless: I admit that I tend to stick to strict semantics on technical questions, and often completely miss the actual intent. Sorry about that.