Code should read like a mathematical proof, exactly because it allows you to follow the steps in between. The requisite granularity of the between steps is com

Code should read like a mathematical proof, exactly because it allows you to follow the steps in between. The requisite granularity of the between steps is completely subjective. If you're catering for the lowest common denominator, then you give up some succinctness, which may be more readable to someone unfamiliar with the concepts, but may just act as a time-wasting loss of abstraction that actually obscures readability to those who are familiar. You wouldn't want me to step through the proofs of associativity and commutativity of addition every time the rule is used, would you? That's why we just prove it once, give it a name, and assume a basic standard of intelligence/familiarity for those who have commit access.