There's no reason a proof has to take *any* time - propositions as types is a to...

ocharles on Feb 12, 2015 | parent | context | favorite | on: A blog engine written and proven in Coq

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.

CompleteSkeptic on Feb 12, 2015 [–]

I think he was referring to the fact that the request completes in finite time isn't a tight enough bound.