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. They are a small variation on the idea of topological space, where instead of defining a space by giving a set of point together with a collection of "open subset" stable under arbitrary union and finite intersection, one instead just give an abstract order set of "open subset" which should have arbitrary supremum and finite infimum and such that binary infinimum distribute over arbitrary supremum. Such a poset is called a Frame, a morphism of frame is an ordered preserving map which commutes to finite infimums and arbitrary supremums. And locales a defined as just being "the opposite of the category of frame" (so a locale is just a frame, and morphisms of locales are morphism 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 subspace, 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 construction form an adjunction between frame and topological space, which can be shown to be an equivalence between rather large subcategory (more precisely between "sober topological spaces" and "spatial locales"). 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 some of them are extremely natural objects and interesting objects (things like the space of "generic real numbers" or the "space of bijection" between two infinite set of different cardinality). Classically, locales and topological spaces are very similar (for example, if you are only interested in complete metric space or locally compact spaces you will not see the differences) but the category of locales is (arguably) slightly better behaved than the category of topological spaces. Constructively, it is a lot harder to construct "points" of locales. This make the gap between topological spaces and locales considerably larger. And locales become incredibly better behaved than topological spaces. For example, 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. I higlhy recommand to have a look to Peter Johnstone excellent introduction paper to the subject ["The point of pointless topology"][4] **2) The localic Zariski spectrum** 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 exemple, one can just says that the poset of open is given by the (oposite) of the poset of 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". This locales we are constructing is still essentially 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. This let you go through with the definition of a scheme in a constructive settings. It appears than most classical results of algebraic geometry became constructive when formulating using locales instead of spaces (and replacing statement involving existence of prime or maximal ideal by statement about property of the 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. **3) Internal logic** The last step to this story relies on "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... but taking complement is a dangerous things in constructive mathematics) 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 exemple, if you prove that some element is nilpotent because it belongs to all prime ideal) become constructive if, instead of chosing a prime ideal, one move to this internal logic and use the universal one. 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. [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