[goto11]

> We simply cannot think about such abstract concepts without introducing some sort of metaphor.

Metaphors are overrated. Often they obscures more than they explain, especially for such an abstract concept.

What if you had to explain "statements" with a metaphor? Or "expression"? I challenge anyone to come up with metaphors which help more than they confuse.

We learn programming concepts through examples, and seeing how they are useful. Not through metaphors.

[Tainnor]

Metaphors are a very powerful tool in human cognition, and there has been a lot of research into their usage from a cognitive science perspective (see e.g. the works by George Lakoff).

Of course, an abstract mathematical proof is independent of any metaphors you may ascribe to them, but new maths is usually discovered by applying intuition to a problem and then verifying that the intuition is in fact correct. To do that, you need metaphors and analogies. The interesting part is when you can use several metaphors for the same concept and the key insight comes from a shift in perspective; e.g. some statements about complex numbers make more sense when viewed from a geometric (rotation-inspired) perspective. Similarly, thinking about e.g. monads as "containers that can be flattened" can lead to certain insights, but thinking about them in some other ways can maybe lead to different insights.

However, I agree with you in one point: we learn mathematics and programming by example; I think the key point is that people have to build their own intuitions and metaphors. It can be useful to guide people along that path, e.g. by pointing out some helpful analogies or dismissing some unhelpful ones, but ultimately, you have to start working with the concept and prove/disprove your own assumptions (this is as true of a new programming concept you're not familiar with yet as of mathematics, only that in the former case you're much less formal about it).

[maweki]

But usually nobody cares about or checks whether your implementation of the operator your overriding still obeys all the axioms. Sometimes we have tests whether some interface implementation fulfills some axioms, but usually we do not.

Somehow with monads we do. And I suspect the reason is, that monads come from an area where of Programming where proving a program correct is preferred to testing. And for proving correctness, you need a proper specification and then implementations that follow that specification. And a specification is done using abstract concepts.

If you want to prove anything about your program (or even understand obscure edge cases), concepts through examples will not work for you.

[marcosdumay]

> But usually nobody cares about or checks whether your implementation of the operator your overriding still obeys all the axioms.

Make some non-associative implementation of (+) and see on how many compilers code using it will work.

[pvg]

"statement" and "expression" in their programming sense are already metaphors.

[goto11]

Well the words are taken from math but means something different in programming. A statement in math have a truth value, so it would actually correspond to an expression rather than a statement in programming.

Saying that a statement in programming is similar to a statement in math (or law or politics or whatever) would be more confusing than informative.

[pvg]

The words are taken from, you know, words. Imprecision can sometimes be more confusing than informative. Are you saying (with a simile?) that the author should have said analogy rather than metaphor?

[goto11]

No, I'm saying the use of metaphors to explain programming concepts is often more confusing than helpful.