Formalizations of the idea that something is a function of something else?
First of all, it seems to me as though the real question here is "what is a variable quantity?" Most of the definitions you quote from pre-20th century mathematicians assume that the notion of "variable quantity" is already understood. But this is already not a standard part of modern formalizations of mathematics; so it's unsurprising that definitions of a subsidiary notion, like when one variable quantity is a function of another one, are hard to make sense of.
So what is a variable quantity? If we want to define the notion of variable quantity "analytically" inside some standard foundational system, then I think we cannot do better than your second suggestion: given a fixed "state space" $A$, an $R$-valued quantity varying over $A$ is a map $A \to R$. Far from worrying that this is historically backward, I think we should be proud that modern mathematics supplies a precise way to make sense of a previously vague concept, and we should not be surprised that in stumbling towards precision people took historically a more roundabout route than the eventual geodesic route that we now know. I think if you pressed any modern mathematician using the phrase "is a function of" to say what they mean by it, this is what they would say (for some suitable $A$, e.g. in "the area of a circle is the function of its radius" the space $A$ is the space of circles, while in "the number of computations is a function of the size of the matrix" the space $A$ is the space of matrices).
However, you seem to be looking for something somewhat different, such as a formalism which the notion of "variable quantity" is basic rather than defined in terms of other things — a "synthetic theory of variable quantities" if you will. Here I think topos theory as well as type theory does indeed help. Given a fixed state space $A$, consider the category ${\rm Sh}(A)$ of sheaves on $A$; this is a topos and hence has an internal logic that is a type theory in which we can do arbitrary (constructive) mathematics. If inside this "universe of $A$-varying mathematics" we construct the (Dedekind) real numbers $R_A$, what we obtain externally is the sheaf of continuous real-valued functions on $A$. Thus, internally "a real number", i.e. a section of this sheaf, is externally a continuous map $A\to \mathbb{R}$, i.e. a real-valued quantity varying over $A$ in the analytic sense. So here we have a formalism in which all quantities are variable. (This point of view, that objects of an arbitrary topos should be regarded as "variable sets" has been promulgated particularly by Lawvere.)
This isn't sufficient to define "function of", however, because as you point out, internally in this type theory, for any "variable quantities" $x,y:R$ there exists a map $f:R\to R$ such that $f(x)=y$, namely the constant map at $y$. If we rephrase this externally, it says that given $x:A\to \mathbb R$ and $y:A\to \mathbb R$, there always exists $f:A\times \mathbb R\to \mathbb R$ such that $f(a,x(a)) = y(a)$ for all $a$, namely $f(a,r) \equiv y(a)$. So the problem is that although $x$ and $y$ are variable quantities, we don't want the function $f$ to be a "variable function"!
Thus we need a formalism in which not only are "variable quantities" basic, there is also a contrasting basic notion of "constant quantity". Categorically, a natural way to talk about this is to think about not just the category ${\rm Sh}(A)$, but the geometric morphism $\Gamma:{\rm Sh}(A)\leftrightarrows \rm Set: \Delta$, which compares the "variable world" ${\rm Sh}(A)$ with the "constant world" $\rm Set$. Just as a single topos has an internal logic that is a type theory, a geometric morphism has an internal logic that is a modal type theory, in which there are two "modes" of types (here the "variable" and "constant" ones) and operators that shift back and forth between them (here the "global sections" $\Gamma$ and the "constant/discrete" $\Delta$).
Now inside this modal type theory, we can construct the object $R^v$ of "variable real numbers" and also the object $R^c$ of "constant real numbers", by copying the usual Dedekind construction in the variable and constant word, and there is a map $\Delta R^c \to R^v$ saying that every constant real number can be regarded as a "trivially" variable one. This gives us a way to say in modal type theory that $y:R^v$ is a function of $x:R^v$, namely that there exists a non-variable function $f:R^c\to R^c$ such that $\Delta f : \Delta R^c \to \Delta R^c$ extends to a function $\bar{f}:R^v\to R^v$ such that $\bar{f}(x)=y$. Or, equivalently, that there is a function $g:R^v\to R^v$ such that $g(x)=y$ and $g$ "preserves constant real numbers", i.e. restricts to a map $\Delta R^c \to \Delta R^c$.
I'm not sure exactly what you hope to achieve with the issue involving assumptions like $y=x^2$ (maybe you can elaborate), but it seems to me that this setup also handles that problem just fine, in roughly the way you sketch: if variable quantities are just elements of $R^v$, then assuming some property of them, like $y= x^2$, doesn't change those elements themselves, internally.
The situation here seems very analogous to that in probability, where there is also a state space $\Omega$ (which is the underlying set of a probability space $(\Omega, {\mathcal B}, {\bf P})$) which is required in the foundations of the subject in order to define everything properly, but is then downplayed as strongly as possible once one starts doing probability. Thus, technically, every random variable $X$ is a function on this state space (e.g., a real random variable would be a (measurable) function from $\Omega$ to ${\bf R}$), but one tries to avoid explicit mention of this space as much as possible, and in fact every so often one actually exercises the freedom to change the state space or probability space, for instance by adding some new sources of randomness, conditioning to an event (somewhat analogous to your equaliser example), and so forth. One can then view probability theory as the study of objects and concepts that remain invariant under a certain type of change of state space, namely that of extending that space; see these lecture notes of mine for more on this (see also these later notes).
One can adapt this viewpoint to non-probabilistic settings. This brings us back to your proposal to view all mathematical objects as depending on a state space $A$, which is not specified precisely and is in fact downplayed as much as possible. One could view this state space as being somewhat dynamic in nature, for instance it could become larger as one makes more measurements in a physical system or introduces some new variables, or it could shrink as one makes some assumptions or fixes some values of certain observables. If one sets things up properly, these evolutions of the state space should not destroy any mathematical facts and relationships one has already gathered about the existing observables: for instance, if two observables $X,Y$ are known to always obey the relation $Y=X^2$, this fact should be unaffected by any changes to the state space caused by performing a measurement of a new observable $Z$, or by making some hypothesis constraining the known observables. (This suggests also to consider some "quantum" version of this setup where making new measurements can destroy the truth of previously established facts... but I digress.)
Incidentally, information theory, which builds upon probability theory, has a well-developed and quite quantitative theory of dependence: for instance, given two discrete (and finite entropy) random variables $X$ and $Y$, $Y$ is a function of $X$ (almost surely) if and only if the conditional entropy ${\bf H}(Y|X)$ vanishes.
When you say "$a$ is a function of $b$", it seems to me that what you're really saying is that "$a$ is independent of $c$" where $c$ is some implicit other part of the context which is somehow "orthogonal" to $b$. It goes without saying that there will typically be other "even more deeply implicit" parts of the context on which $a$ still does depend.
So in type theory, here's how I would formalize it. Let $\Gamma$ be a context, and suppose that
$$\Gamma, b: B, c: C \vdash a: A$$
That is, $a$ is a term (of type $A$) in the bigger context $\Gamma, b: B, c: C$. Then I would say that
$a$ is a function of $b$ (relative to $\Gamma$)
or equivalently
$a$ is independent of $c$ (relative to $\Gamma$)
if the following hold:
We already have $\Gamma, b: B \vdash A$. That is, the type $A$ is independent of $c$.
We already have $\Gamma, b: B \vdash a: A$. That is, the term $a$ is independent of $c$.
This isn't actually a definition internal to type theory, though. So it exists at the same level as the usual "function" definition in set theory (which I would also regard as a perfectly adequate formalization).
In order to get an "internal" definition, you would need to formalize internally what a context is, which seems like overkill to me. I think this is the correct level to define this concept at.
In answer to part of Question 2, I would regard all of type theory, with this formalism of contexts, as a formalism where the notion of "being a function of" is primitive.