5 ms·
The Coq compiler is unverified, it is written in OCaml. It's not possible for Coq's consistency to be verified in itself, thanks to Gödel's second incompletene
by syrak 8y ago
The Coq compiler is unverified, it is written in OCaml.
It's not possible for Coq's consistency to be verified in itself, thanks to Gödel's second incompleteness theorem. However there are still various other aspects of the compiler that could be verified in principle. The CertiCoq project is actively going in that direction.
- quickthrower2 8y agoI love this comment, because there is this pie in the sky mathematical idea, with direct consequences for practical coding.