Since CRDTs are just join-semilattices with a zero element, and the category of join-semilattices with zero is a model for linear logic[1], I suspect that there may be an even cleaner way to write eventually consistent programs, using a linear lambda calculus (or possibly a process calculus, since those also model linear logic). I've been looking into this area in my off-time but haven't managed to get very far, perhaps because I still don't understand category theory well enough. Nice to see there's demand for a language with this property, though :).

[1] Linear logic's "tensor product" corresponds to tensor product of semilattices; linear maps correspond to semilattice-morphisms with a pointwise join operation. Linear "with" and "tensor sum" both correspond to cartesian product of semilattices. It's a rather degenerate model in this respect.