I was thinking about how “mathematical substitutions” make sense as a metaphor for abstraction. Would this sort of thing be helpful? In what contexts? Thinking about how when I use a function as an argument I should be able to “expand” and “collapse” the function to see more verbose versions of it. Is there anything that already does this?

Yeah. Gets a little messy with variable name shadowing, but that can be managed. Is also a good way to negotiate the interface to a function. You know, when you find that some extra bit of context should be passed, especially when that bit wants to be another function.