Have you, since asking the question two years ago, learned about a topos-theoretic treatment of forcing in computability theory?

The thickenings can be much larger than infinitesimal. For instance, the points of the petit Zariski topos of a scheme $S$ are just the set-theoretical points of $S$. The points of the gros Zariski topos of $S$ are local rings $A$ together with a morphism $f : \operatorname{Spec} A \to S$. Any such point determines a set-theoretical point of $S$, by considering the image $f(\mathfrak{m})$ of the unique closed point of $\operatorname{Spec} A$ under $f$. But I find it hard to pretend that $\operatorname{Spec} A$ is an infinitesimal thickening of $f(\mathfrak{m})$.

@h__: I'd like to credit you in my PhD thesis, since your question prompted a short section of it. Please contact me by mail at [email protected] with your realname if you feel comfortable with this.

@HeinrichD: Because for the most part I just summarized the answers given by others in the comments.

Articles by Stefan Schröer and by Ofer Gabber and Shane Kelly discuss the points of the fppf site.

The mapping $U \mapsto S_U$ is a sheaf on $\operatorname{Spec}(A)$, in fact a subsheaf of the constant sheaf $\underline{A}$. It is also called the "universal filter" or "generic filter" of $A$. The structure sheaf can then simply be constructed as the localization $\underline{A}[S^{-1}]$ (performed in the internal language of the topos of sheaves over $\operatorname{Spec}(A)$).

Hakim's thesis is indeed a treasure trove. But she doesn't use the internal language at all, which was not yet developed at her time. With the internal language, some of her constructions and proofs can be simplified; for instance, her very general spectrum functor from ringed toposes to locally ringed toposes is given by interpreting a (constructively sensible formulation of the) usual spectrum construction in the internal language. The universal property of the construction then follows from the well-known universal property of the usual spectrum.

@nfdc23: The key reason why the proof of Grothendieck's generic freeness lemma is much easier using the internal language is that the structure sheaf $\mathcal{O}_X$ looks like a Noetherian ring and in fact like a field from the internal point of view, even if the scheme $X$ is not locally Noetherian. This simplifies the situation to the easiest nontrivial case (from an arbitrary not necessarily Noetherian base ring to a field). This fact doesn't have any concise external counterpart: neither the sets $\mathcal{O}_X(U)$ nor the stalks $\mathcal{O}_{X,x}$ are Noetherian or fields.

A friend and I turned two of Andrej's great ideas into talks at the Chaos Communication Congress. For anyone interested in our take on these topics, for instance for giving similar talks, recordings are here: Four dimensions, Infinity. It's helpful to imagine the infinitely many persons to be sitting in the "magical bus of Harry Potter" which has finite length from the outside but is infinitely large from the inside. This way $\omega+1$ is easily visualized as a further person waiting behind the bus.