Some theorems are stated and proved extensionally, but in practice are almost always used intensionally. Let me give an example to make this clear -- integration by parts:
$$ \int_a^b f(x)g'(x)ds = \left[f(x)g(x)\right]_a^b - \int_a^b f'(x)g(x) dx$$
for two continuously differentiable functions $f$ and $g$. In practice, this is seldom ever applied to *functions* but rather to *expressions* denoting functions. Much more importantly, it is almost always applied by 'pattern matching' on a product *term*. But note that integration is usually described formally as an operation on *functions* (i.e. extensional objects), but then in first-year calculus the students are taught to master a series of rewrite rules (i.e. operations on intensional objects).

Logicians [Leibniz, Frege, Russell, Wittgenstein, Quine, Carnap to name a few] have worried a lot about this. Linguists [Montague comes to mind], and physicists [A. Bressan] have worried about this too.

I have two questions:

- What other examples have you run into of such mixing of extension and intension?
- Why is this dichotomy not more widely taught / appreciated?

In the case of algebra (more precisely, equational theories), the answer to #2 is very simple: because this dichotomy does not matter at all, because we have well-behaved adjunctions between the extensional and intensional theories [in fact, we often have isomorphisms]. For example, there is no essential difference between polynomials (over fields of characteristic 0) treated syntactically or semantically. But there is a **huge** difference between terms in analysis and the corresponding semantic theorems.

2more comments