I am interested in type theory and proof theory. I have read a lot of papers and books that use the term "computational content" (For example: https://scholar.google.com/scholar?hl=en&q=%22computational+content+of%22&btnG=&as_sdt=1%2C33&as_sdtp=) and I have developed an intuitive sense of the meaning, but I have never seen the term formally defined.
Is anyone aware of a paper or book which defines this term?
Let me respond to your comments to Bjorn and Matt's answers:
Let's say I have a sentence of the form $\forall x\exists y\theta(x, y)$, where "$\theta(x, y)$" is "simple" (say, only bounded quantifiers) - I'm not interested in how hard it is to evaluate $\theta(a, b)$ for a given $a, b$. Then a computational interpretation begins with Skolemization: we look at the sentence $$\exists F\forall x(\theta(x, F(x))).$$ We're interested in what sorts of $F$ work here.
One reasonable question to ask is, Can such an $F$ be given by an algorithm? This yields a distinction between "computably true" sentences and "not computably true" sentences.
But as you correctly observe, this is a very coarse distinction in many cases. We often care about the runtime of an algorithm, or its complexity in some other sense (e.g. space used). So we may ask: "Is there an $F$ which works which is in $\mathcal{C}$?" for some nice complexity class $\mathcal{C}$.
We may also be interested in provable correctness. Maybe there's a polynomial-time computable $F$, but proving that this $F$ works requires large cardinals :P. It would be quite reasonable to say that this is pretty bonkers. So now we're interested in the theories within which statements like "There is a polytime-computable solution" are proved.
And, finally, we may also run into the opposite problem: given two non-computably true sentences, we may want to argue that one is "more computably true" than the other. To do this we now need to compare noncomputable functions, e.g. via Turing reducibility. So we can also go to a "larger" context, and work there. (See e.g. this paper, and also reverse mathematics.)
All of these concerns - the complexity of Skolem functions, and the difficulty of proving such complexity results - are broadly part of one intuition: that our desire to prove a theorem does not stop only at determining its correctness. I would call all the nuances of a theorem, in this sense, its "computational content" - and since this is so broad, I would not hope for a formal definition of this term. (You could create one, but I think it would necessarily lose some of the aspects of the term. Not everything has to be formalized, and I say this as a formalist!)
For all the titles on the first page of that link, "the computational content of $x$" means "the extraction of algorithms from $x$".
For instance, from an intuitionist proof of $\forall a \ \exists b$ you can extract an algorithm from $a$ to get $b$. Even from a classical proof of $\forall a \ \exists b$, some of this papers show how to extract an algorithm from $a'$ to get $b'$, at least in the right contexts.
A key early proponent of this concept was Georg Kreisel, who gave this statement of the goal and a proposed definition in 1958: “to determine the constructive (recursive) content or the constructive equivalent of the non-constructive concepts and theorems used in mathematics, particularly arithmetic and analysis....The concept of recursive interpretation is intended to give a precise formulation of the notion of constructive content (equivalent)." Solomon Feferman's 1996 commentary offers context.
I don't think it's supposed to be a formal notion. But for instance for a statement like $\forall a\exists b $, the computational content could be: how hard is it to find that $b $. Is $b $ a computable function of $a $, for example.
