5 ms·
"The great mathematician and founding figure of computer science, Alan Turing, showed that it is impossible to eliminate all errors from software." Oh? I thoug
by pcvarmint 15y ago
"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 15y agoIndeed, 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.