There's no reason a proof has to take any time - propositions as types is a tool to guide us to correct information flow, it doesn't mean we literally run the p

There's no reason a proof has to take any time - propositions as types is a tool to guide us to correct information flow, it doesn't mean we literally run the proof at every step. If we trust the core, we can erase the proof checking at the point of compilation and we're left with identical machine code that has been proven to do exactly what we expect and specify.