I'm still an undergraduate student but I would like to show my point of view.
The construction of mathematics is based on axioms, that is the lowest level possible you can reach; once logic bases are established it is possible building things at higher level using theorems. I think of theorems in mathematical sense as functions in programming: you have some conditions and from these you can show a result in a new, different form through a chain of logical steps of axioms and results of other theorems; on the other hand functions in programming work the same: they get keywords, variables and other functions to compute the needed result.
While learning the mathematics we don't learn its low-level structure, while it could have sense seeing from how logically the mathematics is built but we start from something close to our common experience and then build the knowledge over the knowledge we already have; on the other hand we cannot start learning programming from assembly even if its performance are the best and we can know exactly what is happening inside the program, it would be an overkill!
Making an example would be useful.
Take for example the definition of indefinite integral for function $f: \mathbb{R} \to \mathbb{R}$ (function $f$ that inputs a number and returns a number):
$$\int f(x)\, dx$$
Was is it? The inverse operator of derivation, so:
$$\int f(x)\, dx = F(x) + c \text{ so that } \frac{dF(x)}{dx} = f(x)$$
but was the derivation operator (for $f: \mathbb{R} \to \mathbb{R}$) is?
$$\frac{dF(x_0)}{dx} = \lim_{h \to 0} \frac{f(x_0+h) - f(x_0)}{h}$$ for $x_0 \in \mathbb{R}$. Then extend it for $\forall x_0 \in \mathbb{R}$ where to limit exists.
But we are using limits: what are they?
$$\lim_{x \to c} \, f(x) = l$$
is
$$\forall \epsilon > 0, \exists \delta > 0, \text{ such that } |x-c|<\delta \Rightarrow |f(x)-l| < \epsilon$$
But we are using inequalities, that is a characteristic of $\mathbb{R}$ (real numbers), so we can describe $\mathbb{R}$ is a field that has a total order ($<$ operator).
- field is a ring with some properties (won't describe in depth);
- a ring is are two groups with some interesting properties too (won't describe in depth too);
- a group is couple (for example $(\mathbb{R}, +)$, $(\mathbb{R}, \cdot)$) for which some properties are true (won't describe in depth too again);
We could ask what $+$ and $\cdot$ are: they are functions that do some stuff (examples: $2.1 + 5.4 = 7.5$, $\pi \cdot \pi = \pi^2$) from a set ($\mathbb{R} \times \mathbb{R}$) to another set ($\mathbb{R}$).
Continuing, a fuction is a collection of all couples (for example for $+$ is $((\mathbb{R} \times \mathbb{R}) \times \mathbb{R})$ such that the relationship given by the function between members of the couples is true (example: $4+6 = 10$ so $((4, 6), 10) \in A$ where $A$ is set of all couples that make $+$ function true).
And what $\mathbb{R}$, $(\mathbb{R} \times \mathbb{R})$, $((\mathbb{R}
\times \mathbb{R}) \times \mathbb{R})$ are? Talking broadly they are sets that have special properties (for example $(\mathbb{R}, \mathbb{R})$ is a set that cointains all couples real numbers, such as $(\pi, 3)$, $(0,0)$, $\dots$).
It's also worthy to say that $\mathbb{R}$ set is a "generalization" of the natural numbers set $\mathbb{N}$ and natural numbers are the starting point.
But there are still questions: what is a set and how natural numbers can be constructed? A simple answer to explain a set can be done by saying it's a
container that can contain everything with no distinction of exactly same elements.
To define natural number set we can use set theory definition (see also):
\begin{align}
0 &= \{\} \\
1 &= \{0\} = \{\{\}\} \\
2 &= \{0,1\} = \{\{\}, \{0\}\} = \{\{\},\{\{\}\}\} \\
3 &= \{0, 1, 2\} = \dots
\end{align}
We still go further and ask how could we define a set better or how can we logically explain demonstrations and its forms (for example induction proofs)... In this case things like ZFC, Gödel and other interesting things emerge.
In this point have probably arrived to "assembly" of math starting just a single from a "high-level function" (math-programming comparison intended).
