Also relevant: the paradox doesn't apply in point-free topology, because it allows for "locales" that doesn't contain any points but still have nonzero measure. So rather than giving up axiom of choice, we may instead accept that "a set of points" doesn't quite correspond to the intuitive notion of a shape.
Any suggestions for (as a CS person who has been finding quantales useful for my favourite applications, and is curious as to whether there may be connexions to other disciplines) getting into point-free topology?
Second this, because I'm no mathematician myself and it doesn't look like there are much layman-available material out there. "Point-free" is also another name for tacit programming (i. e. without assigning names to variables, like Forth or bash pipelines), but I can't find any reference on if it is just named for superficial similarity or is there some deeper theoretical connection between point-free topology and point-free programming.
In the tacit programming case, I'm pretty sure it's for (a) superficial resemblance, and (b) the excuse to call one's favoured technique "pointless programming".
(there's probably something interesting to be gotten at by considering how much violence a particular function does to structure in the input space —thinking of compositions of homomorphisms being homomorphisms of compositions, or how mapping a monotonic function over keys allows one to avoid reindexing— but I'm pretty sure that's mostly orthogonal to whether one binds parameter names or not)
