Most modern mathematicians don't work with foundations but it was a hot topic at the beginning of the 20th century. Most mathematicians today wouldn't even be able to tell you when they are using the axiom of replacement, an important but technical piece of ZFC. Before the work on foundations mathematicians frequently relied on intuition to explain their ideas. The point of mathematical precision is to be able to transmit mathematical ideas with fidelity to other mathematicians; common intuitions are important for that even today.
However, it is frequently the case that mathematical intuition breaks down and paradoxical ideas need to be reckoned with. One historical example is Weierstrass's "monster": a function that is everywhere continuous but nowhere differentiable. The intuition at the time was that a continuous function could only fail to be smooth at a set of isolated points, a very tame set. It is no coincidence that he came up with this example in a period when his school was trying to recast calculus on more rigorous footing.
As for the motivation for founding mathematics on formal systems, it's because set theory is so useful for writing down mathematical ideas but naive set theory is plagued with contraditions, such Russel's paradox. Common language, too, is afflicted with contradictions such as Richard's paradox. The question was how to separate the wheat from the chaff so one does good mathematics and not nonsense. Influential mathematicians like Hilbert set out programs to establish set theory and arithmetic on a sound footing so that its use would not be held suspect. This required a more thorough mathematical development of logic as started by Boole, Frege, and others (my recollection of the precise history of these ideas is vague at this point).
So concurrently we saw the mathematization of logic, arithmetic, and language and the establishment of a reasonable set theory that did not give rise to antinomies. None of the answers were entirely satisfactory but they were good enough that common mathematical activity could continue without too much doubt. When there are questions of precision, one tries to fall back on the informal mathematical language of sets which is commonly presumed to be formalizable in systems such as ZFC.
A lot of development since then in formal mathematical systems has to do with the study of computation and the mechanization of mathematical reasoning.
However, it is frequently the case that mathematical intuition breaks down and paradoxical ideas need to be reckoned with. One historical example is Weierstrass's "monster": a function that is everywhere continuous but nowhere differentiable. The intuition at the time was that a continuous function could only fail to be smooth at a set of isolated points, a very tame set. It is no coincidence that he came up with this example in a period when his school was trying to recast calculus on more rigorous footing.
As for the motivation for founding mathematics on formal systems, it's because set theory is so useful for writing down mathematical ideas but naive set theory is plagued with contraditions, such Russel's paradox. Common language, too, is afflicted with contradictions such as Richard's paradox. The question was how to separate the wheat from the chaff so one does good mathematics and not nonsense. Influential mathematicians like Hilbert set out programs to establish set theory and arithmetic on a sound footing so that its use would not be held suspect. This required a more thorough mathematical development of logic as started by Boole, Frege, and others (my recollection of the precise history of these ideas is vague at this point).
So concurrently we saw the mathematization of logic, arithmetic, and language and the establishment of a reasonable set theory that did not give rise to antinomies. None of the answers were entirely satisfactory but they were good enough that common mathematical activity could continue without too much doubt. When there are questions of precision, one tries to fall back on the informal mathematical language of sets which is commonly presumed to be formalizable in systems such as ZFC.
A lot of development since then in formal mathematical systems has to do with the study of computation and the mechanization of mathematical reasoning.