Is there any such formalization of the process of abstraction? You know, in the same way there is a formalization of lambda calculation via the lambda calculus?

If not, couldn't there be?

It's one thing to understand a program, another thing to abstract, another thing still to understand and reason about the process of abstracting during program development. If there were an 'abstraction' calculus, maybe it would be easier to teach engineers about abstraction as well as when and how to do it?