[pcvarmint]

"The great mathematician and founding figure of computer science, Alan Turing, showed that it is impossible to eliminate all errors from software."

Oh? I thought he only proved that it's impossible for an algorithm to determine whether an arbitrary program will halt -- not whether all errors can be eliminated from software.

[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.