The reason to use formal systems is to be able to reason about larger, more complex systems. Our brain is rather limited and to empower ourselves, we've found the divide and conquer approach. For that to work, we need assurances that our composition is correct due to the subcomponents being correct (and the composition operator). This is something we do all the time. You assume your compiler is correct, or your common libraries. However, if we want to grow larger systems, our foundations become more critical and we need stronger assurances.