It seems to me that junk theorems are fundamentally a manifestation of leaky abstractions. It happens when you can see the implementation details from inside the abstraction.