Yes, that&#x27;s exactly what I meant. But compare this to CompCert. CompCert itself is verified, which means it doesn&#x27;t have to output a proof for each program it compiles.<p>Even if you don&#x27;t care about the theoretical concerns of for all vs for each, there are two practical concerns with this kind of system. 1) the compiler could just fail to output a valid proof for some program and you&#x27;re out of luck until the compiler bug is fixed. 2) Proof checking can get pretty time intensive and it&#x27;d be better to do it once for the compiler, than every time you run the compiler.