I agree. It’s kind of like secure boot, in reverse: the high level stuff has to ...

		brookst 30 days ago \| parent \| context \| favorite \| on: Lean proved this program correct; then I found a b... I agree. It’s kind of like secure boot, in reverse: the high level stuff has to be complete and correct enough that the next level down has a chance to be complete and correct.