The goal of the contract system is that you give a specification of behavior and you specify the boundary between who has to provide one side of that behavior and who has to uphold the other side. The point of the paper I linked to, and lots of other work on contract semantics, is to decide what that idea means in tricky cases in a principled way, rather than just saying that more checks are good or more checks are bad. You could always change the enforcement strategy to just skip checks every seventh time, but that seems wrong. And the best way we have of answering these questions says that ->d is wrong, in the same way the skip-every-seventh approach is wrong. So that’s why it’s deprecated.

It’s of course reasonable to think that the costs of being correct in this case are too high to be worth paying, just like you might think that about a checked version of C.

But that isn’t the perspective of the designers of the contract system.

At this point I think I’m more or less satisfied with the idea that contracts themselves are checked in a principled way that more or less corresponds to “as strictly as possible,” but that they’re not placed at the tightest possible boundaries. I get the impression that’s the right conclusion for me to reach about the intentions of the design and the way the system is used, and I don’t have objections to the big picture of it. I have some sticking points on smaller parts of the topic though.

I agree that a strategy that skips checking is wrong. This itself is why I was originally wondering why there’d be such a preference for contract-out, but I’m basically satisfied with the idea that it’s comprehensive about checking for a certain non-comprehensive boundary.

I would think that if the contract says explicitly that every seventh check is skipped, then an enforcement strategy that doesn’t skip is wrong.

Originally, I thought ->d was sufficiently explicit about skipping, and hence that calling it buggy was a misunderstanding of its purpose.

Now, my remaining faith in ->d as a potentially acceptable design is the possibility that there’s no innate checking that it would need to skip in the first place.

Going back to that example from the docs…

     #:pre
     (zero? (f #f))
     any)

The contract (-> integer? integer?) is intended to describe the mediation between the client and the server. It’s quite useful to allow it to mediate between the client and the contract as well, the way ->i works. However, if a different kind of mediation is desired there, ->d allows that to be expressed seamlessly, while ->i interferes and needs to be routed around.

…Actually, ->d isn’t quite the right design for this either, because I would prefer for noncompliant values of f to be blamed on the client, not on some define/contract form that’s inside the ->d contract.

All right, let’s say my remaining faith in ->d is basically at zero now. :smile: There are operations like ->d that I might have faith in, but ->d itself doesn’t provide the tools I would hope for for these use cases.

There’s another sticking point remaining in my mind around define/contract. It seems to skip the checking of some uses of the definition (namely, recursive ones). Is there an ongoing or historical reason justifying that, or could this be an actual mistake?

The behavior of define/contract is intentional. The whole idea is that a contract goes at a boundary between the creator and the client. For contract-out, those are the defining module and the using module. For define/contract it’s the function definition and the rest of the world. So the recursive use is inside the boundary and other uses are outside the boundary.

All right, I suppose my intuition is that all uses of the defined variable are clients, and hence that any place where these clients can be located must be outside the contracted region, even if that means the contracted region needs to be a shape with holes in it. I can kind of imagine treating definitions as mini-modules where there’s an inner binding that happens to be named the same thing as the binding everyone else sees, but I don’t know what the point of that is. Maybe just a difference in intuition?

Thinking of them as mini modules is the correct intuition. There’s even the with-contract form for doing it more generally

I was wondering if the reason might be keeping tail recursion cheap. There may be other mechanisms like collapsible contracts to keep that cheap now, but it seems like it could have been a historical justification…

If you think of define as expanding into a letrec, then define/contract puts the contract boundary around the whole letrec. The version where the recursive call is checked would put the boundary around the lambda on the RHS of the letrec

Part of the justification of using modules as contract boundaries is that it’s a less expensive boundary

But I don’t think that’s part of the reasoning for define/contract which has never been a big part of the design

Thanks for talking me through these things. I appreciate it. :)