To add to Simon's comments, here is a concrete example where taking global elements does not commute with exponentials. The global elements of the NNO $N$ of the effective topos are the plain old natural numbers $\mathbb{N}$. However, not every set-theoretic map $\mathbb{N} \to \mathbb{N}$ is the induced map on global elements of a morphism $N \to N$ of the effective topos. Those induced maps are exactly the computable maps, but not every set-theoretic map is computable.

Regarding applications of topos theory, what about the classical examples such as crystalline cohomology or elucidating realizability and studying higher-order computability via the effective topos? For a recent and minor example, what about the proof of Grothendieck's generic freeness theorem using topos-theoretic methods (Section 3.5 in the linked notes)? Perhaps you can clarify your questions a bit so we can give more directed answers :-)

Parts of your questions are answered in Sections 1.1f. of this note of mine. Briefly: Allowing locales without points streamlines the theory, helps massively in constructive mathematics (including relative mathematics over a base space) and is crucial for certain representation theorems in topos theory (for instance for showing that for any object $X$ of any topos $E$, there is a surjection $f:F\to E$ such that $f^*(X)$ is countable, namely the classifying $E$-locale of surjections $\mathbb{N}\to X$. This locale doesn't have any points if $X$ is uncountable)

Addition a couple years later: It is worth noting that Baer's criterion does not require LEM, only Zorn's lemma. (Zorn's lemma and the axiom of choice are equivalent only iassuming LEM. Without LEM, AC implies Zorn but not the other way round.) This observation is good to know because while almost no topos validates Zorn+LEM (= AC), assuming Zorn in the metatheory, there is a plenitude of toposes which validate Zorn, namely at least the localic toposes.

@MircoA.Mannucci The decomposition theorem (via the Smith normal form of integer matrices) has a constructive and predicative proof, hence holds internal to any elementary topos (and even internal to any arithmetic universe). By interpreting the proof in the effective topos, we obtain an algorithm for carrying out the decomposition; by interpreting the proof in a sheaf topos, we obtain a version of the decomposition for continuous families of finite(ly presented) groups.

Among others, a relevant reference is Fred Richman's The Fundamental Theorem of Algebra: a constructive development without choice (link).

There is a very nice concept of 'toposes [with NNO but] without subobject classifiers', namely the arithmetic universes pioneered by Joyal and studied by Maietti, Vickers and recently Alexander Oldenziel. While the initial elementary topos with NNO is a souped-up version of Heyting arithmetic, the initial arithmetic universe is a souped-up version of PRA.

... can be phrased in the internal language, that is Theorem 8.3 in my thesis). In the case $X = \mathrm{Spec}(R)$, you could internally to the topos $\mathrm{Sh}(X)$ consider the constant sheaf $\underline{R}$, but modules over it are not particularly interesting. The structure sheaf $\mathcal{O}_X$ is not $\underline{R}$, but a certain localization of $\underline{R}$ (the localization at the "generic prime filter" -- a filter which does not exist in $\mathrm{Set}$, but does exist in $\mathrm{Sh}(X)$).

I believe that the other comments already resolved most of your questions, right? If not, please indicate where you'd appreciate additional detail. Regarding your question on internal categories: The external category of all sheaves of $\mathcal{O}_X$-modules (not only the quasicoherent ones) is internally the category of all $\mathcal{O}_X$-modules (where now $\mathcal{O}_X$ is a plain old ring, not a sheaf). The external category of quasicoherent $\mathcal{O}_X$-modules is internally a certain subcategory of that category (the condition for a module to be quasicoherent ...

@user20948: Yes! If $\mathcal{E}$ classifies a theory $\mathbb{T}$, the slice $\mathcal{E}/X$ classifies "$\mathbb{T}$ adjoined by a constant $x:X$". This makes sense because the object $X$ of $\mathcal{E}$ can be obtained from the generic $\mathbb{T}$-model by geometric constructions (small colimits, finite limits). Hence a sort "$X$" together with appropriate auxiliary sorts, function symbols and axioms can be added to $\mathbb{T}$ in such a way that the interpretation of this sort "$X$" in any $\mathcal{E}$-topos $\mathcal{F}$ is precisely (the pullback to $\mathcal{F}$ of) the object $X$.

Welcome to MO, Lereau! Thank you for the apt summary of the proof, and for bringing paper (2) to my attention. A further very nice related paper is Arithmetic is Categorical by Benno van den Berg and Jaap van Oosten. But can you clarify what exactly you are asking? :-)

Yes, we can! For instance, the same internal proof shows that, in AG, the Grassmannian is a smooth scheme over the base, and in DG, the Grassmannian is a smooth manifold (see Section 20.3 of these notes of mine). However, as you say, this approach is limited, the internal world of the toposes used in AG does differ quite a bit from their DG counterpart. For instance, in the toposes for AG, any map $R \to R$ is a polynomial. A generalization of this observation is the basis for synthetic AG, yet totally false for SDG.

To clarify: The sign function only seems to defy the cited classical falsehood. It doesn't really, as it cannot be shown to actually be a function $R \to R$. Regarding your greater question: I tried to give a short answer in Section 4.5. Briefly: both.

If you want to see a couple of examples for the wondrous non-classical facts holding in specific toposes, you can have a look at these notes of mine, particularly Section 2 and Section 3. I am happy to any questions you might have concerning these notes!

The excellent survey by Mike Shulman at arxiv.org/abs/0810.1279 presents a couple of options for set theories to use for category theory.