In [Theory mainly concerned with lambda-calculus?](https://mathoverflow.net/questions/11845/theory-mainly-concerned-with-lambda-calculus/11861#11861), 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?



Is functional programming a branch of mathematics?
So, I'm a computer scientist working in this area, and my sense is the following: 


You cannot do good work on functional programming if you are ignorant of the logical connection, period. However, while "proofs-as-programs" is a wonderful slogan, which captures a vitally important fact about the large-scale structure of the subject, it doesn't capture *all* the facts about the programming aspects. 


The reason is that when we look at a lambda-term as a program, we additionally care about its *intensional* properties (such as space usage and runtime), whereas in mathematics we only care about the *extensional* properties (i.e., the relation it computes).[\*] Bubble sort and merge sort are the same function under the lens of $\beta\eta$ equality, but no computer scientist can believe these are the same algorithm.


I hope, of course, that one day these intensional factors will gain logical significance in the same way that the extensional properties already have. But we're not there yet.


[\*] FYI: Here I'm using "intensional" and "extensional" in a difference sense than is used in Martin-Lof type theory. 


