Let me wrote a quick introduction to this idea:


**1) Locales**

I do not know if you are already familiar with the notion of locale that Andrej is referring to in his talk: They are a small variation on the idea of a topological space, where instead of defining a space by giving a set of points together with a collection of "open subsets" stable under arbitrary unions and finite intersections, one just gives an abstract ordered set of "open subspaces" which should have arbitrary supremums and finite infimums and such that binary infinimum distribute over arbitrary supremum. Such a poset is called a Frame (this is actually the same as a complete Heyting algebra), a morphism of frame is an ordered preserving map which commutes to finite infimums and arbitrary supremums. And locales are defined as just being "the opposite of the category of frames", i.e. a locale is just a frame, and morphisms of locales are morphisms of frame in the other direction.

It is rather easy to go from a topological space to a locales by just remembering the poset of open subspaces, and attaching to a continuous map its action on open subset by pre-image.
Conversely if one has a locale $X$, one can define a "point" of it as a morphism from the locale corresponding to the one point topological space to $X$, there is a topology on this set of points (generated by the element of the frame corresponding to $X$) and these two constructions form an adjunction between locales and topological spaces, which can be shown to be an equivalence between rather large subcategories. More precisely it induces an equivalence between "sober topological spaces" and "spatial locales", where spatial locales are the locales "having enough points" in a precise technical sense.

There are however some locales which have no points at all. At first you can regard them as pathological monster, but it in fact appears that at least some of them are extremely natural and interesting objects (things like the space of "generic real numbers" or "random real numbers" that Andrej mentioned in his talk, or the "space of bijection" between two infinite set of different cardinality whose non triviality is the key points for Cohen forcing to works).

Despite this, classically, locales and topological spaces are very similar (for example, if you are only interested in complete metric spaces or locally compact spaces you will not notice the difference) but the category of locales is overall (arguably) slightly better behaved than the category of topological spaces.

But constructively, it is a lot harder to construct "points" of locales and a lot more locale appears to be non-spatial. This make the gap between topological spaces and locales considerably larger. And in this weaker framework, locales become incredibly better behaved than topological spaces. For example without the law of excluded middle the correct definition of the locale of real number might be non-spatial but is always locally compact, while it is well known that constructively the topological space of real numbers can fail to be locally compact (this is one of the bad things that happen in constructive analysis that Andrej mentioned in his talk). In fact it is known that they agree if and only if the topological space of real number is locally compact.

Similarly, a lot of classical theorem which requiert the axiom of choices become fully constructive when formulated in terms of locales. This the case for example of the [Tychonov theorem][1], [the Hahn Banach theorem][2], or the [Gelfand duality][3].

For example the idea for the Hahn Banach theorem is that instead of asking for the existence of certain linear form or extension of linear form, we construct a space (a locale) of linear form and show that this is not the empty space (even if it might not have points) and that the map between these spaces induced by restricting to a subspace is always a "surjection" in a good localic sense. And this roughly also what happen for the Gelfand duality or the case of ring spectrum that we will discuss below

I highly recommend to have a look to Peter Johnstone excellent non technical introduction paper to the subject ["The point of pointless topology"][4] which will expand on what I just said. and probably explains it more clearly.



**2) The localic Zariski spectrum**

So, the starting idea is that one can construct the Zariski spectrum of a ring, together with its structural sheaf directly as a locale without ever mentioning prime ideal or maximal ideal. For example, one can just says that the poset of open is given by the poset of radical ideal of the ring. One can also give a presentation by generator and relation of the corresponding frame which is more convenient to work with. This is done for example in section V.3 of P.T.Johnstone's book "Stone spaces". And while prime ideal are a little dangerous constructively as they might not exists, ideals are not problematic at all, you always have plenty of them.



This locale we are constructing is still morally the "space of prime ideal of the ring" but the question of whether the ring actually has any prime ideal or not become just the question of whether this space has points or not, which a rather unimportant question in locale theory.

In fact, if you are familiar with the notion of classifying topos, it is the "space of prime ideal" in the sense that it is the classifying space for prime ideal, more precesely for "prime ideal complement", i.e. subset $O$ of the ring such that ($xy \in O \Rightarrow x \in O \text{ and }y \in O$;  $0 \notin O$; $1 \in O$ ; $x+y \in O \Rightarrow x \in O \text{ or } y \in O$) which classically are exactly the complements of prime ideal, and construcively are more important because they are the things you need to get a locale ring when localizing.


This let you go through with the definition of a scheme in a constructive setting. It appears than most classical results of algebraic geometry became constructive when formulated using locales instead of spaces (and replacing statement involving existence of prime or maximal ideal by statement about property of this "space of prime ideals" similarly to the Hahn banach theorem above). Unfortunately, except very basic things, these are mostly "folk theorem" and do not very often appears in literature (because let's face it, not many algebraic geometer are interested in constructivisme...). With the exception of the work of Ingo Blechschmidt that I mention below.

In fact (but that is a personal opinion) I've always found that, for someone already familiar with locale theory, the localic treatment of the basic property of the Zariski spectrum are notably simpler than their usual topological treatment. 


**3) Internal logic**

The last step to this story relies on the use of "internal logic". The idea is that if you work internally in (the topos of sheaves over) the localic Zariski spectrum, then you actually have a "prime ideal of your ring" (more precisely, you have a "localizing system" which satisfies the properties to be the complement of a prime ideal mentioned above) and this prime ideal is in some sense the universal prime ideal of your ring (proving a property for this internal prime ideal proves property for all prime ideal of your ring) and a large number of proof that relies on the axiom of choice because they says at some point "let M be a maximal/prime ideal of your ring" (for example, if you prove that some element is nilpotent because it belongs to all prime ideal) become constructive if, instead of choosing a prime ideal, you move to this internal logic and use the universal one.

This produces a quite efficient and automatic method to make lots of results of algebra and algebraic geometry constructive.

This idea of exploiting internal logic in algebraic geometry tend to make everything constructive and has been pushed quite far by Ingo Blechschmidt (you can watch one of his talk [here][5], or read his thesis work [here][6])

To my knowledge the work of Ingo is the only place where you will find a non trivial treatment of algebraic geometry which use this picture.


For another example, another place, completely different from prime ideal, where you will use non-constructive things in algebra or algebraic geometry is when you want to talk about algebraic closure of a fields. But it appears that this point of view also provide a solution. In general you cannot construct a single algebraic closure of a given fields, but what you can instead do is to consider the "space of all algebraic closure of the field" in the sense of theory of classifying topsoes. This times this will not even be a locale, but a more general kind of topos, and it appears that this topos is something that have actually been studied a lot by algebraic geometers: indeed, if you start from some ring $R$ and study the "space of all algebraic closure of all residual fields of $R$" defined in a proper way what you get is nothing else than the "small étale topos of $R$". See the [work][7] of Gavin Wraith on the subject.


  [1]: https://eudml.org/doc/211282
  [2]: https://ac.els-cdn.com/000187089190082I/1-s2.0-000187089190082I-main.pdf?_tid=f2e35626-c9ef-11e7-8060-00000aacb360&acdnat=1510741987_bddfd6d825e5fa9b29bd90c3e8ad6f74
  [3]: https://ncatlab.org/nlab/show/constructive+Gelfand+duality+theorem
  [4]: http://pointlesstopology.com/the-point-of-pointless-topology.pdf
  [5]: https://www.youtube.com/watch?v=7S8--bIKaWQ
  [6]: https://github.com/iblech/internal-methods
  [7]: https://link.springer.com/chapter/10.1007/BFb0061844