The very notion of a "non-leaky abstraction" is a tool that is only just beginning to be employed by programmers. At its most advanced level you're talking about bisimulation proofs over abstract data types.
We may get there one day, but for right now just spec'ing interfaces as combinations of consistent laws is a stretch.
I'm not sure that's true. It would certainly be an interesting anthropological undertaking to pin down the details, but (at substantial risk of being wrong) I feel like this was an assumption in early attempts at abstraction and we only feel the need to specify "non-leaky" because we have discovered important things that previous attempts have - in practice - tended to leak.
I think I'm in agreement with you here—we're slowly, as a community, discovering how to make non-leaky abstractions. They've been around for a while in places where "in practice" had a lot of legroom (pure mathematics). CS has a lot of legroom too, but it's taken a long time for us to think about it in such a way to know where we can place our weight.
Comments
The very notion of a "non-leaky abstraction" is a tool that is only just beginning to be employed by programmers. At its most advanced level you're talking about bisimulation proofs over abstract data types.
We may get there one day, but for right now just spec'ing interfaces as combinations of consistent laws is a stretch.
I'm not sure that's true. It would certainly be an interesting anthropological undertaking to pin down the details, but (at substantial risk of being wrong) I feel like this was an assumption in early attempts at abstraction and we only feel the need to specify "non-leaky" because we have discovered important things that previous attempts have - in practice - tended to leak.
I think I'm in agreement with you here—we're slowly, as a community, discovering how to make non-leaky abstractions. They've been around for a while in places where "in practice" had a lot of legroom (pure mathematics). CS has a lot of legroom too, but it's taken a long time for us to think about it in such a way to know where we can place our weight.