Your point about equating f . id = id is related to what the equality sign means. Presumably you don't object to the notion that sin(a + b) = sin(a) cos(b) + c

Your point about equating f . id = id is related to what the equality sign means. Presumably you don't object to the notion that sin(a + b) = sin(a) cos(b) + cos(a) sin(b), even though the left and right hand sides are totally different in terms of computation. That's because you know that such identities, while indeed abstracting over computational details, have real meaning and are extremely useful in mathematical thought (and algorithm design; you can use that equation to implement an efficient numeric oscillator). Given that you probably accept that trigonometric equality, you can't really dismiss equational reasoning in software as useless just because it abstracts over stack frames and machine instructions. That kind of abstraction is exactly the point.