We need to shatter the programming / mathematics binary
Many of us programmers approach our craft just like mathematics (including equational reasoning, proofs, and category theory)
Comments like these come across as a snide erasure of our experiences
Conversation
Replying to
Reading about the Curry-Howard correspondance shattered the dichotomy for me. Like have you ever written a function? Or used them? Yep you just proved theorem
3
1
8
I think what means is that for the majority of programs C-H is not interesting. If you're writing code where "can i find a function relating these types?" is something you need to think about, you're writing pretty involved "mathy code" already.
1
2
Most code has a flavor "of course there is a function, i just need to figure out how to write it down practically".
1
If you can write code where functions actually carry some real meaning as proofs, great!
If not, then types might not be the right way to encode meta properties, and other mathematical methods might be better.