alt Hacker NewsWhat I’m wondering about is why we don’t need to understand/verify the generated kernel and only the spec?
Is there an implicit trust we must put in that kernel?
What I’m wondering about is why we don’t need to understand/verify the generated kernel and only the spec?
Is there an implicit trust we must put in that kernel?
The implementation of a function is in the CSG/Impl folder. A proof is in the CSG/Proof folder. They are both imported and tied together in the human reviewed file in a theorem that makes a mathematical statement about the function. Lean checks mechanically that the theorems are proven via the supplied proofs. Here you have to trust the Lean checker, but neither the proof nor the implementation.
Then you know that the statement in the file you reviewed holds about that function.