“You might think, well that’s just common sense. But last I checked, computers don’t have common sense. Indeed, they must have a formal way to automate these kind of code optimizations. Maths has a way of formalizing the intuitive, which is helpful amidst the rigid terrain of computer logic.”
— Mostly Adequate Guide to Functional Programming on Wadler’s free theorems
λ ∧ ¬λ 