The Two Abstractions of System Design: Hide or Reduce

The article distinguishes between two types of abstraction in system design: modularity abstraction, which hides internal details behind interfaces to simplify usage, and modeling abstraction, which reduces a system to its minimal behavioral skeleton to expose and leverage concurrency. The author argues that while computer scientists are trained in modularity abstraction, modeling abstraction—essential for formal methods like TLA+—requires a different skill set focused on identifying what should "leak" to prove invariants. This cognitive dissonance explains why many struggle with modeling, as it crosscuts system organization rather than encapsulating it.

When talking about TLA+, I keep referring to "abstraction" as the most important thing to learn. And it is about the hardest to learn as well. But a contradiction has been bugging me. Aren't CS people already supposed to be good at abstraction? Isn't abstraction supposed to be at the root of OS, networking, software engineering? Abstract Data Types ADTs are a staple of every in CS curriculum. So why do I and every other formal methods/modeling person see such a large skill gap in abstraction, and flag it as the core, make-or-break skill for modeling? I think I finally get to the root of this cognitive disonance. There are two kinds of "abstraction" conflated under the same umbrella term. These two couldn't be further apart in terms of their goal Let me try to explain in the next two sections. Modularity abstraction is about interfaces that hide internals. Modeling abstraction is about behaviors, and about reducing a system to its minimal behavioral skeleton for the property you care. Modularity abstraction encapsulates, draws a vertical boundary, and hides the layer below. Modeling abstraction is crosscutting: it slices the system along a behavioral plane and keeps only what is absolutely relevant to the property under investigation, and even then in the form of "what", not "how". This slice usually looks nothing like the system's organization. Modularity abstraction is all about sealing the leaks, hence Joel Spolsky's famous post lamenting that "all abstractions are leaky". Note that his list is all about modularity abstraction: TCP hide IP , string libraries hide character arrays , file systems hide spinning disks , virtual memory / flat address space hide MMU and paging , SQL hide query plans , NFS / SMB hide the network , C++ string classes hide char . Modularity abstraction aspires to hide the interleavings and present operations as if they were atomic. Its goal is to make the module easy to use, but in doing so it forgoes exposing concurrency or efficiency opportunities. In stark contrast, the modeling abstraction is about identifying what should leak and leveraging it It exposes the fine-grained actions and orderings, and proves that invariants hold despite the interleavings. The payoff for this work is to harvest the maximum safe concurrency from the system. There is an abundance of modeling abstraction in distributed systems field. It feels like almost all protocols are designed this way.