Indeed, it was the Curry–Howard correspondence which led to the realisation that...

lubutu on Feb 22, 2012 | parent | context | favorite | on: D-Wave Defies World of Critics With ‘First Quantum...

Indeed, it was the Curry–Howard correspondence which led to the realisation that software could be proven correct: a function's type can be seen as a proposition, the function itself a proof of that proposition.