[lubutu]

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.