matteocapucci
Joined 6 years ago
Karma
26
Submissions
11
Member since
Aug 29
Joined 6 years ago
The fact it's so rare to find a counterintuitive fact in CT, so that you rarely find yourself proving something and you mostly spend your time constructing effective tools, it's a feature not a bug! McBride's "Don't touch the green slime!" is a great paper/saying about this principle. Work with the compiler, not against it. The compiler is very dumb so it understands only trivial things.
There's a legacy pseudomachist culture of 'hard is good' in mathematics (but really, it's transversal to science) which rewards working hard and not working smart.