3 ms·
It is a lot like how you have to trust the core proving kernel in a theorem prover but if you do then you can trust every proof created using it.
by UltraSane 1y ago
It is a lot like how you have to trust the core proving kernel in a theorem prover but if you do then you can trust every proof created using it.
- burnt-resistor 1y agohttps://github.com/CertiCoq/certicoq https://github.com/CertiCoq/certicoq can prove (most of) itself.