Certainly there are three parties (that’s the whole point of that paper). Obviously what contracts do is part of the specification, but that doesn’t mean that we can’t say that one specification is better than another.

However, I don’t think it makes sense to talk about whether individual contracts “project” in different directions. Individual contracts mediate between particular values and their contexts.

You talked about a value flowing from one side a boundary to another.

In two-sided boundary situations, in terms of what I understand from the Racket docs, such a value arrives on the other side of the boundary as another value, namely the one that’s output by the contract’s “projection.” On a casual look, I don’t see the verb “project” in the docs outside the noun “projection,” so perhaps I backformed it.

At risk of putting words in your mouth, I get the impression I should describe the projection as a function that takes an unmediated value and produces a mediated one. I still think that for thin API-boundary-only contracts, I could appreciate having less expensive mediation policies apply when a value passes through to the contract level, and I’m still inclined to describe that in terms of the direction a value traverses a contract boundary in.

Perhaps the explanation I’m looking for is that using contracts at strategically chosen boundaries (contract-out) is a natural way to cut down on unnecessary checks, and that but that if and when contracts are used, they’re meant to act comprehensively. Is it something like that?

There’s still a part of this that I’m not making total sense of yet, because another natural way to avoid unnecessary checks is to specify a more permissive contract, and that’s what I think ->d is. Perhaps this part just has to do with the fact that ->d has a name that doesn’t make its permissiveness sufficiently obvious.