To write a formal (computer checkable proof) you must justify every single step of reasoning all the way down to the axioms of the foundation. Of course that would make proving simple things like $((ab)cd)e = a(bc)(de)$ a terrible chore requiring repeated applications of the associativity (infact proving something as simple as $1 + 100 = 101$ could require $100$ applications of the definition of plus!). The idea of reflection is to reduce trivial reasoning steps to computation, This is described in Section 4 of Henk Barendregt's Proofs of correctness in Mathematics and Industry, but it was also applied heavily in a recent formal proof of the four color theorem.