From my limited understanding, I think contract-out would create a new identifier, bind it to the contract-attached value and provide it rename-out, something like (provide (contract-out [f ctc])) (define f ...) ;=> (provide (rename-out [outside-f f])) (define f ...) (define outside-f (contract ctc f pos-party neg-party))

but I think the actual outside-f is much more complicated since the negative party is only known when the current module is required by its client. I don’t know the full story there.

say, outside-f is probably actually a transformer that when expanded will turn into the real contracted value