soft question - 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 $betaeta$ 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.