Rearranging across the interface

Rearranging across the interface

No, for performance reasons. We inline parts of our libraries (even in C, where the inlined parts go in the .h file) into their callers because the result of doing so is a massive performance boost from the optimizer - which can do things like reason "hey, len can't be zero here, so I can eliminate the code that handles the empty list case completely".

To get the sort of boundary you're describing, we do static linking and carefully hand-crafted interfaces for plugins. That's the state of play today, for everything from assembly through C to Agda and Idrs; the goal, however, is to dynamically link, which means that we need to go deeper. And then we have a problem, because the moment you go deeper, your boundaries stop applying, thanks to inlining.