Is there any good way to explain formally what functions are?
What I mean is that the understanding is usually rooted in set theory, saying that a function from a domain set to a codomain set is a certain kind of subset of their Cartesian product set. This just seems to be a kind of example of a function though, in the same way that a Dedekind cut or an equivalence class of Cauchy sequences of rational numbers are examples of real numbers within set theory. In that case I can check that the set of each such structure has the correct properties of the axiomatically defined real ordered field when the appropriate arithmetic and order relation are added.
I wonder if we can explain exactly what functions have to look like, other than by explaining it in everyday language, so that we can prove that the "model" of functions that resides in set theory indeed satisfies the desired axiomatic properties.
You might be interested in ETCS, the 'Elementary Theory of the Category of Sets'. It's a theory of sets, but it doesn't use membership as a fundamental concept. Instead it uses functions. Functions aren't defined as a subset of the cartesian product, they're simply taken to be fundamental objects. Then there are axioms describing how functions behave and what their properties are, and everything else is built up from that.