Most #IT#coders have never heard of Curry-Howard isomorphism between type theory and proof theory (type (\equiv) proposition, programme (\equiv) proof), which #programmers in #Maths and #CS have exploited for decades.
Knowing the techniques is well and good, but understanding the theories matters, at least as much.
Add comment