Darboux's Integral vs. the "High School" Integral

As you noted, Darboux's definition uses the infimum and the supremum throughout, which is not a concept one usually studies at highschool. Moreover, the definition using the mesh of partitions going to zero is somewhat messy when it comes to rigorous work, and it somewhat difficult to verify integrability using it versus Darboux's criterion. However, it is quite convincing for students to consider the integral as an approximation using sums of rectangles, so the "high school" definition may be more natural at first. It is sensible that in favour of good definitions, books such as Spivak's Calculus use Darboux's definition which gives a cleaner exposition.

One can look into more details that show why Darboux's definition is (maybe) better. For each $\delta >0$ one can define $U_\delta=\{P\text{ is a (tagged) partition of } [a,b]:\lVert P\rVert <\delta\}$. Observe that $\delta_1<\delta_2\implies U_{\delta_1}\subseteq U_{\delta_2}$, so every set is comparable with each other, and $\bigcap_{\delta >0}U_\delta=\varnothing$. In this sense, we say the collection $\{U_\delta:\delta >0\}$ defines a direction on the set of partitions of $[a,b]$. Observe how punctured balls $B'(x,\delta)$ define a direction in the set of nbhds of a point of a metric space, or how the tails $\{n,n+1,n+2,\ldots\}$ define a direction in the set of natural numbers.

With this in mind, we would say $I=\displaystyle\int\limits_a^b f$ if for each $\varepsilon >0$ there exists $U_\delta$ such that for any $P\in U_\delta$, $|R(f,P)-I|<\varepsilon$. Again, this is a bit problematic: we need to pick an arbitrary partition and an arbitrary set of tags and find a suitable candidate for $I$, and verify the inequality for any partition of this kind.

On the other hand, we know that $\sup_PL(f,P)$ and $\inf_P\{U(f,P)\}$ always exist, and we have a theorem which asserts that $L(f,P_n)\to \underline{\int_a^b f}$ for a sequence of partitions $P_1,P_2,\ldots$ provided only that $\lVert P_n\rVert \to 0$. This helps greatly in the evaluation of integrals, the same claim holding for $U(f,P_n)$. This is in fact the theorem one uses (maybe unknowingly) when evaluating the integral of say a continuous function by means of regular partitions and limits of Riemann sums.

Moreover, Darboux's idea translates to the (very useful) criterion of Riemann, namely, that for each $\varepsilon >0$ we can find two partitions $P,P'$ such that $$U(f,P)-L(f,P')<\varepsilon$$

This in turn translates to a more geometrical picture: that for each $\varepsilon >0$; we can find step functions $s,t$ with $s\leqslant f\leqslant t$ and $$\int_a^b t-\int_a^b s<\varepsilon$$

In fact, one can check that $$\overline{\int_a^b}f=\inf_{f\leqslant t}\int_a^b t$$ $$\underline{\int_a^b}f=\sup_{s\leqslant f}\int_a^b s$$

where $s,t$ are always step functions. This idea somewhat passes over to Lebesgue's integrals, which might also give Darboux's insight another point. Darboux's integral is indeed equivalent to Riemann's integral.

The morale is, maybe, it is always easier to work with suprema and infima rather than with any kind of limits. The former are usually much more well behaved and lead to simpler proofs, for example.

A comment on

"...especially because it seems to take considerably more time to construct."

I would say a reason why Darboux's definition is more useful is precisely because one has taken the time to carefully construct it!