Computation is a sibling (or maybe child) of logic, it is not a superset of logic. I like Wadler a lot and get that the Curry-Howard isomorphism makes it tempting to view them as the same thing, but logic is field of far vaster proportions and history. I think "computer science" is properly called computability theory.
The proposal in the HN title is a bit like saying "calculus should be called mathematics".
Try programming in a proof assistant to see how inseparable computation and logic are. It gets more fundamental than the Curry-Howard correspondence when homotopy type theory enters the scene.
Comments
Computation is a sibling (or maybe child) of logic, it is not a superset of logic. I like Wadler a lot and get that the Curry-Howard isomorphism makes it tempting to view them as the same thing, but logic is field of far vaster proportions and history. I think "computer science" is properly called computability theory.
The proposal in the HN title is a bit like saying "calculus should be called mathematics".
Try programming in a proof assistant to see how inseparable computation and logic are. It gets more fundamental than the Curry-Howard correspondence when homotopy type theory enters the scene.