Which is why this kata should not be translated to some languages.

Actually, no... I don't think what you're describing is quite what I was thinking of originally. But whatever its behavior is, it makes sense.
The difference, I guess, is that in the stack-popping model, before doesn't always propagate past lambda. It only affects variable accesses that would be "free" if the thing inside before stood as an expression on its own.

Ah, that makes sense. I was thinking about something like that. What you describe seems equivalent to propagating an extra before into each variable expression, which I had considered but dismissed as too ad hoc. Your explanation makes much clearer what's going on and why this is sensible behavior. Thanks!

While before (lambda here) is perhaps sensibly disallowed, it actually does have a sensible interpretation too. If you think of de Bruijn indices as providing a "stack" of arguments in context then before pops the stack before continuing into a subexpression. So, for instance

lambda (before (lambda here))   ~   flip const

In other terms, before will "shield" a subexpression from one level of context.

I'm a little confused about the interface described in Language -- it seems to indicate that nonsensical programs such as before (lambda here) are allowed, and the example tests don't say anything about such programs. Do I need to read the paper to figure out how to handle these, or are they just supposed to crash?