I need to dive into it.

Do you mean it because of the formal logic being used?

This is because compilation can be represented as a finite sequence of applying simple rewrite rules. You don't need a true Turing-complete language to do so, because you don't have any indeterminate loops in such process. Any simple total language (like Coq) is more than enough.