4 ms·
You don't even need a Turing-complete language for writing compilers, see CompCert for example.
by sklogic 12y ago
You don't even need a Turing-complete language for writing compilers, see CompCert for example.
- pjmlp 12y agoI need to dive into it. Do you mean it because of the formal logic being used?
- sklogic 12y agoThis 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.