Philosophically there are problems in abstractions of mechanisms.
A scheme that does work is to implement abstractions only in terms of previously implemented abstractions.
In this plan each abstraction can be assigned an integer level and the implementation of each abstraction is allowed to use only abstractions whose level is less than its own.
This precludes recursion and several other useful software patterns—but it is easy to understand.
Digression
The foundations of mathematics struggled to overcome this problem and the term predicative arose to describe the simple finite tower of abstractions alluded to above.
Actually the term impredicative is used for abstraction schemes that do not follow the discipline.
Here is a history of the mathematical struggle.
This note describes how Keykos made sense of two abstractions, A and B, each of which formally relies on the other.
The solution there is to describe three layers B', A and B to which we assign levels 0, 1 and 2 respectively.
B' is like B but missing some semantics—a deficient form of B.
B' is good enough for the purposes of A however.
This now clearly conforms to the predicative discipline.
It is now observed that B and B' can share code—indeed they are the same code and a correctness proof must show that when A invokes B it uses only that subset of B’s code that implements the B' semantics.
I suspect that just about any complex system plays such tricks and that the virtual predicative nature of the layering is only in the heads of a few of the original designers and is seldom documented.
I am sure that there are undocumented pseudo circularities in Keykos.
When I have noticed such circularities in Keykos I have been able to apply this analysis.
About the last feature of the factory was the ability to create cycles of factories thus violating the formal predicative rule.
The familiar factorial definition:
int fac(int n){return n?n*fac(n-1):1;}
is impredicative and requires a heavier duty argument.
No finite number of fictitious abstractions suffice, but 12 abstractions suffice when you consider that fac works only for arguments less than 12 in case of 32 bit ints.