MathOverflow will be down for maintenance for approximately 3 hours, starting Monday evening (06/24/2013) at approximately 9:00 PM Eastern time (UTC-4).

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.