In [Theory mainly concerned with lambda-calculus?][1], F. G. Dorais wrote, of the idea that the lambda-calulus defines a domain of mathematics:

> That would never stick unless there's another good reason. Besides, the schism between cs and math is very recent, I would contend that "functional programming" is actually a math term, historically speaking. More importantly, it would be wrong to use a term different than those who use it most, namely theoretical computer scientists, who are very competent mathematicians by the way. 

The idea, I think, is that the overlap between the kind of constructive mathematics that follows the formulae-as-types correspondence, and pure functional programming is so substantial that the core of the two topics is essentially the same subject.

Is this true?

  [1]: http://mathoverflow.net/questions/11845/theory-mainly-concerned-with-lambda-calculus/11861#11861