I wanted to learn more about the internal language of of toposes and to do so I have been reading both Sheaves in Geometry and Logic (Sheaves) by Mac Lane and Moerdijk and Introduction to Higher Order Categorical Logic (HOCL) by Lambek and Scott. Both texts develop the internal logic of a topos in different ways. In particular, Sheaves interpret variables x of type A as the identity map on A, while HOCL interprets such an x as an indeterminate $$x:1 \rightarrow A.$$
Is there any benefit to using either approach? From searching around on the internet, it seems that the method used in Sheaves is more common. There is a discussion about this issue here, however they pretty much ignore the approach in HOCL.
What other sources are recommended for someone wanting to learn about this further?
Because I think a result central to Lambek & Scott's approach is interesting, I've decided to try and consolidate my comments into an answer.
It's natural to think of variables in a formula as sort of "virtual constants," in the sense that we can think of the formula is definitely making a statement about "things", but we're being as vague as possible about which things. From this perspective, the approach in Lambek & Scott is conceptually fairly natural if you're on board with the notion of a constant being a function on a nullary product, because the idea is just that we add, by a free construction, a new constant of the type we want and try to make it devoid of any extra properties.
The drawback is that (1) an "indeterminate $x:1\to A$" in their sense is not actually a morphism in the topos we're studying--or at least, not a morphism $1\to A$ in that topos--and (2) fiddling around with these indeterminates means taking a detour through some much more involved theory than we do in Mac Lane & Moerdijk to really see how it ticks. Point (2) is perhaps the most damning part, because one of Lambek & Scott's results actually assures us that their approach gives us the same information as that of Mac Lane & Moerdijk.
The gist of why this works comes from the main theorems of I.6 and I.7 in Lambek & Scott (the latter of which is essentially the same approach as the linked nLab article in the comments). This is the "functional completeness" result that means that, for a Cartesian closed category $\mathcal{E}$ and indeterminant $x:1\to A$ in what they call the "polynomial category" $\mathcal{E}[x]$, there is a correspondence between morphisms $B\to C$ in $\mathcal{E}[x]$ and $A$-parameterized maps from $B\to C$ (i.e. maps $A\times B\to C$) in $\mathcal{E}$. That is, a map with free variable $x$, $f(x):B\to C$ in $\mathcal{E}[x]$ corresponds by cartesian closedness to a morphism $\bar{f}:A\to C^B$, which is what you'd expect a free variable of type $A$ to mean under the Sheaves in Geometry and Logic interpretation. In particular, the projection $p_A:A\times 1\to A$ corresponds to an indeterminate $\pi:1\to A$ that, in some sense, is maximally general: for $g:A\to B$ a morphism in $\mathcal{E}$, $g\circ \pi:1\to B$ in $\mathcal{E}[x]$ just corresponds to $g$ again in $\mathcal{E}$--which is to say, composition of $g$ with $id_A$.
I like this result because it means there is a link between our "virtual constants" and "parametrizing functions" views of variables; and looking at (what is essentially) weakening and contraction operations via comonads has some very interesting generalizations. But in practice, if you want to use the internal language to say things about toposes, then it's a few extra steps in the translation that you would quickly learn to do without.