I have seen this figure of speech in multiple places. But to be specific, in the book 'Type Theory and Formal Proof: An Introduction' we have the following example which derives a type judgement, using 'flags', that is 'assumptions' that are then 'discharged' using the abstraction rule:
\begin{align} (a)\;| &\quad \text{Flag:}\; x:A \\ (b)\;|&\quad|\quad \text{Flag:}\; y:B \\ (1)\;|&\quad|\quad x:A & \text{(var rule on (a))} \\ (2)\;|&\quad \lambda y:B. x: B \to A & \text{(abst rule on (1))} \\ (3)\;\, &\lambda x:A\;\lambda y:B. x: A \to B \to A & \text{(abst rule on (2))} \\ \end{align}
This is then expressed in words, considering propositions as types and inhabitants of propositions as proofs (PAT interpretation):
\begin{align} &\text{(a) Assume that $x$ is a proof of proposition $A$.}\\ &\text{(b) Also assume that $y$ is a proof of proposition $B$.}\\ &\text{(1) Then $x$ is (still) a proof of $A$.}\\ &\text{(2) So the function mapping $y$ to $x$ sends a proof of $B$ to a proof of $A$}\\ &\quad\quad\text{i.e. $\lambda y:B.x$ proves the (logical) implication $B \to A$}\\ &\text{(3) ...} \end{align}
I have no problem with any of this reading except for the the part: $$ \text{the function mapping $y$ to $x$ sends a proof of $B$ to a proof of $A$} $$
What is a function doing sending proofs to proofs? or is it types to types? Can it send any proof to any proof? Is this specific to propositional logic? Is this is feature of abstraction? Is this abuse of language? Where does it come form?