@nfdc23: Sorry, I only noticed this thread now. Your question is of course a very valid one. My favourite example for where the approach using the internal language really shines is Grothendieck's generic freeness lemma in complete generality (for not necessarily Noetherian reduced rings). The proof using the internal language is short and simple (Section 11.5 in my notes), but all external proofs I know are not very straightforward and proceed using a series of reduction steps.

I'm really grateful for your question! It provided motivation for my PhD thesis; in particular, I tackled question 2. The internal logic of T has a distinctive algebraic flavor, for instance in that any internal function $\mathbb{A}^1 \to \mathbb{A}^1$ is a polynomial. I referenced your question in a talk of mine.

@Steven: Yes, you can solve the size issues with Grothendieck universes (if you are willing to use them); but if you want the big Zariski topos of $\operatorname{Spec} A$ to classify local $A$-algebras, then you need to use the site consisting of finitely presented $A$-algebras. Bigger sites will yield nonequivalent toposes.

I too agree that it's an excellent resource for learning topos theory. It's not a terrible suggestion at all.

Very good question. Unfortunately I don't know the answer. I suspect that even in the case that $M$ is the terminal prime system ($M_x = \operatorname{Spec} \mathcal{O}_{X,x}$ for all $x$), where Gillam's localization coincides with Hakim's spectrum functor, the result can fail to be a scheme. But I don't really know.

$\mathbf{Set}^\mathrm{op}$ is equivalent to the category of complete atomic Heyting algebras (you may read "complete atomic Boolean algebras" here, if you're willing to work in classical logic) and therefore concrete as a subcategory of a concrete category.

More details on my previous comment are now available in the section on the relative spectrum in these notes of mine. The category of locally ringed spaces is a coreflective subcategory of the category of ringed spaces, but note that it's not a full subcategory, so the usual statements about limits and colimits in (co-)reflective subcategories don't apply.

I agree that the intuition "continuous family of sets" is somewhat vague. Sure, there are skyscraper sheaves, where stalks jump from ${*}$ to a larger set. This kind of jump is acceptable, whereas the jump from $\emptyset$ to a larger set is not. I appreciate the thought you're putting into the question! I like your idea with jumps from 1 to 2. However, the argument "$i_* i^{-1} \mathcal{F} \cong \mathcal{F}$" breaks down, since it's no longer true that the only nontrivial stalk of $\mathcal{F}$ is at $x$.

I agree with Dan (even though I would have quite liked to have my question resolved with a simple example!). The failure of $\mathcal{E}$ to be a sheaf can be explained geometrically: Recall that there is the familiar saying "a sheaf is a continuous family of sets". This is one of the few times where this saying is strinkingly vivid. The family which is $\{\star\}$ at $x$ and $\emptyset$ at all other points is not continuous in an intuitive sense of the word.

Indeed. And a reason why one needs stability under pullback is in order to be able to construct the sheafification functor.

This comment probably won't help you, but it might help others with a similar question: A way of calculating Ext groups in Serre quotient categories is demonstrated by Mohamed Barakat and Markus Lange-Hegermann.