I posted this question on MSE a few days ago, but got no response (despite a bounty). I hope it will get more answers here, but I'm afraid it might not be appropriate as I'm not sure it's actually research-level. Please do tell me if it's not appropriate and if possible tell me how to modify the question so that it may become appropriate (if such modifications exist)
I recently saw a video of a presentation of Andrej Bauer here about constructive mathematics; and there are two examples of locales he mentions that strike me : he explains quickly what the space of random reals might be, by saying that it's the locale of reals that are in every measure $1$ subset of $[0,1]$ (for instance): as he says, of course there are no such reals, but that should not stop us from considering the space of these reals, which may have interesting topological properties even if it has no points.
Similarly in a constructive setting (or classical setting without AC) some rings may have no prime/maximal ideals, and so their spectrum as usually conceived is uninteresting. But that should not stop us from studying the space of prime/maximal ideals with the Zariski topology, even if it has no points.
My questions are related to these examples specifically and to generalizations:
Is the first example of random reals in any way connected to the random reals one mentions in forcing ? e.g. is forcing to add some random reals in any way connected to considering the topos of sheaves on the locale of random reals ?
Has the second example been extensively studied ? What sort of properties can we get from the study of this "Zariski locale" ?
Is there some form of general theory of locales as spaces of imaginary points ? For instance is this how one usually sees locales intuitively; or better is there some actual theory (more than a heuristic) of constructing pointless (or with few points) spaces of objects that we'd like to exist but don't actually exist ? This is very vague so I'll give a further example of what one might envision: if two first-order structures $A$ and $B$ aren't isomorphic but $A\cong_p B$, we might want to study the space of isomorphisms of $A$ and $B$, which would ideally be a pointless locale. One could say something similar about generic filters of a poset when one is trying to do some forcing : from the point of view of the small model, these generic filters don't exist: we could envision a space of generic filters. In these four cases we have some objects that don't exist (random reals, maximal ideals, isomorphisms) but that we can define and that in some very vague sense ought to exist, and so we construct the space of these objects; but it turns out that this space can have no points at all: is there a general theory of this sort of thing ?
These questions are very vague so I hope they're appropriate. I'll appreciate answers with references, but I'd also very much like answers that themselves provide some intuition (though a bit more technical than what I've expressed in the question), and some thoughts.