my takeaway was modularity abstraction (as the author describes it) hides implementation and modeling abstraction reduces the system to the min. behavioral state required to preserve your invariants
https://muratbuffalo.blogspot.com/2026/08/composition-and-mo... The rely-guarantee reasoning we used in this post is where the two abstractions meet and become a joint constraint. The modularity abstraction is the boundary: we split the specs into private versus interface variables, hiding produced from the consumer and consumed from the producer. The modeling abstraction is the Env actions. E.g., EnvPut is not an API for the producer, it is a reduction of the producer: the minimal behavioral skeleton of the entire producer relevant to the consumer's property.