Localic locales?  Towards very pointless spaces by iterated internalization. One can think of locales as (generalizations of) topological spaces which don't necessary have (enough) points.  Of course when one studies locales, one "actually" studies frames,
certain sorts of lattices, but reverses the arrows so that story has a less algebraic and more geometrical/topological flavor.
So while "localic spaces" make lack for a "sufficient" set of point, by their very nature they do have a sufficient set of "open sets" (scare quotes because these open sets arise as a primitive notion and not as actual sets of anything).

Curiosity drive us on: could one go a step further and make the open sets of locales as ghostly as locales make the points of spaces ghostly?

Let me put the question more technically (but correct me if you think now that I'm asking the wrong question):  One often interprets algebraic objects such as "group objects" in sufficiently nice categories.  So locales with ghostly open sets might show up as localic locales, or what amounts to the same, "coframic frames" -- diagrams in the opposite category to the category of frames, specifically diagrams that define internal frames.  Though such things must have at least two points (the empty set and the total space) corresponding to the nullary operations in the algebraic theory (just as a localic group must have at least one point, the identity, a priori it seems that they might have no more.
In this spirit

How would one construct interesting examples of coframic frames = localic locales?

Even if such things have few classical points, and few classical open sets, they will still have plenty of classical (open) sets of open sets.  

By what formalism might one keep on going, iterating the internalization?

The previous question implicitly suggests levels of internalization indexed by natural numbers?

Could someone propose a definition for a level of internalization indexed by a limit ordinal?

 A: Let me give an example of a category whose objects should be thought of as being “localic locales.”
Consider the category $\mathcal{F}_{U}$ consisting of all pairs $(X,M)$ where $X$ is a set and $M$ is an ultrafilter on $X$. If $(X,M),(Y,N)$ are objects in $\mathcal{F}_{U}$, then a function $f:X\rightarrow Y$ is said to be a morphism if $f^{-1}[R]\in M$ whenever $R\in N$. Let $\mathcal{G}_{U}$ be the quotient category $\mathcal{F}_{U}/\simeq$ where if $f,g:(X,M)\rightarrow(Y,N)$ are morphisms, then $f\simeq g$ if and only if $\{x\in X\mid f(x)=g(x)\}\in U$. This category was originally formulated in Andreas Blass's dissertation.
One should consider the objects in $\mathcal{G}_{U}$ as being open set free locales. If $(X,M)$ is an object in $\mathcal{G}_{U}$, then the “points” in this “space” are the elements in the intersection $\bigcap M$. If $M$ is non-principal, then $\bigcap M=\emptyset$, so the “space” $M$ is completely point-free. The “open sets” in the “space” $(X,M)$ are the equivalence classes in $P(X)/M$. In this case, $(X,M)$ only has two points, namely $X/M$ and $\emptyset/M$.
The category $\mathcal{G}_{U}$ even has its own version of Stone-duality since the dual of $(X,M)$ will be an ultrapower $\mathcal{A}^{X}/M$ for a suitable structure $\mathcal{A}$.
A: First off, let's forget the transfinite iteration. As David said, one often interprets algebraic objects such as "group objects" in sufficiently nice categories, intending the word "group" as a cipher for any kind of algebra, so let's also say "space" for any object of any kind of "sufficiently nice" category. Monads provide a notion of "algebraic theory" that can be interpreted in any category.
So we can formulate the question more abstractly by asking for a category $S$ (whose objects we call "spaces") for which the opposite category $S^{op}$ is equivalent to the category of algebras for a monad on $S$ (and we call these algebras "frames").
This is exactly the idea behind my Abstract Stone Duality research programme, which was so called because both the duality between algebra and geometry and the "always topologize" slogan behind David's question were due to Marshall Stone.
In the ASD programme I developed this idea in the case where the adjunction between $S$ and $S^{op}$ is given by the exponential $\Sigma^{-}\dashv\Sigma^{-}$, where I write $\Sigma$ rather than Todd's 2 for the Sierpinski space.  These ideas are summarised from a foundational point of view in Foundations for Computable Topology. Mathematically, the pay-off of the monadicity hypothesis was a theory of computable analysis that satisfies the Heine-Borel theorem, for which see The Dedekind Reals in Abstract Stone Duality with Andrej Bauer. This was applied to the intermediate value theorem in A Lambda Calculus for Real Analysis, which paper is the best introduction to ASD for ordinary mathematicians.
This idea works properly for
Computably Based Locally Compact Spaces.
Can we do something similar taking $S$ to be the category of locales, to get back to David's question? Indeed, Steve Vickers has studied this,
using his double powerlocale monad.   (I find this easiest to understand as the comonad on frames that arises from the forgetful functor to dcpos.)  He uses the name localic locale an object of the opposite of the category of algebras for the monad over locales (or a coalgebra for the comonad on frames), although he has also called them colocales and I like this name myself.
We therefore have the categories $L$ of locales and $C$ of colocales, where $C^{op}$ is monadic over $L$, but they are not equivalent. David may therefore ask what the iteration of this construction yields, but in fact it stops at stage 2: $L^{op}$ is also monadic over $C$.
Even so, this cannot be the end of the story, because we would like $L$ and $C$ to be subcategories of a single cartesian closed category with finite limits.  Steve has used the presheaf category for this and shown that the monad is actually the double exponential in this sense. Reinhold Heckmann constructed a smaller category of equilocales.  However, the structure of these two categories is far more complicated than that of equilogical spaces.
I am currently studying another categorical idea called equideductive logic, the slogan for which is "a category that lies nicely within its cartesian closed extensions". As in Steve's work, the double exponential brings you back into the smaller category, but I also ask that any subspace of an object in the smaller category (ie an equaliser targeted at any object of the larger category) also lie in the subcategory. 
A: Here are some ruminations which might point in a reasonable direction. 
By analogy with how one thinks of power sets, and power sets of powers sets, etc., as higher-order set-theoretic constructions, I would be tempted to term these things "higher-order locales". And in parallel with set theory, a "full" second-order locale would be constructed as an exponential $2^X$ where $X$ is a locale and $2$ is Sierpinski space, if this exponential exists. For if it does exist, then points $1 \to 2^X$ are in bijection with morphisms $X \to 2$, which are in bijection with the original "open sets" of $X$ (that is to say, elements of the associated frame). 
It is a theorem that this exponential $2^X$ exists, i.e., that a locale $2^X$ exists such that maps $Y \to 2^X$ are in natural bijection with maps $Y \times X \to 2$ (naturally in $Y$), if and only if the locale $X$ is locally compact. A full account is given in Johnstone's Stone Spaces. It is relevant for this discussion that if this particular exponential $2^X$ exists, then any exponential $Y^X$ exists. 
We might just take a moment to explore the sense in which this leads to locales in the category of locales. Following Lawvere, we may define the notion of internal frame as follows: let $E$ be any category with arbitrary small products. Then a frame object in $E$ is a product-preserving functor 
$$FreeFrame^{op} \to E$$ 
where $FreeFrame$ is the Kleisli category for the monad on $Set$ whose algebras are frames, i.e., the full subcategory of $Frame$ whose objects are free frames on sets (the free frame on a set is the frame whose elements are downward-closed sets in the poset of finite subsets of $X$). For an exposition of this general point of view, one could try the nLab article on algebraic theories, which is basically a working out of the theory of infinitary Lawvere theories (which you may well know already, David, since you were a student of Linton and he was really a founding father here). 
Anyway, one way of constructing frame objects in $E$ is by constructing product-preserving functors $F: Frame^{op} \to E$, because the composite 
$$FreeFrame^{op} \hookrightarrow Frame^{op} \stackrel{F}{\to} E$$ 
is then also product-preserving. Now of course $Frame^{op} \simeq Loc$; thus we are here contemplating product-preserving functors 
$$F: Loc \to E$$ 
and in particular, we can consider the case where $E = Loc$. Then, if $X$ is a locally compact locale, the exponential functor 
$$(-)^X: Loc \to Loc$$ 
is product-preserving (in fact, it is a right adjoint to $- \times X$, hence preserves all limits). One can use this as a stepping-stone to construct other frame objects in $Loc$ since the category of frame objects in $Loc$ is complete and cocomplete. 
(And then, of course, we define $Loc(E) = Frame(E)^{op}$, and so we have some techniques for constructing, as a special case, localic locales.) 
People do like to play with second-order locales to prove various interesting results. Here is an interesting paper by Martin Escardo (written 'spatially', but I believe Martin likes to think 'localically'), which develops the idea that Theo touched upon in his comment under the question, on compactly many intersections of opens. Johnstone's Elephant also utilizes such techniques, as in the proof of C3.2.8 (which I learned from Mike Shulman under this Math Overflow question). 
I've not thought about transfinite iteration of frame-internalization. 
A: Yes - you can have localic locales and 'localic localic locales' etc. The process stops at the second stage where you find you get back to the category of locales which I personally find a remarkable result. The result is by Vickers - I am not sure if he published it; I believe there is a categorical proof of it in the DRAFT version of 'weak triquotient assignments in locale theory' on my website (www.christophertownsend.org). Note, however the definition of a localic locale in this context is an algebra of the double power locale monad - this might not be exactly the notion you are after but I would say is the 'best' definition of what a locale should look like internal to the category of locales.  
