> I'd daresay is the majority opinion among mathematicians. It is also the opinion of prominent computer scientists: Dijkstra, Leslie Lamport, Donald Knuth, to name a few off the top of my head.
There are reasons partly historical and partly due to the subject matter of CS that mathematicians closer to it tend to place relatively higher value on formality.
> It is also plainly true: mathematics is about rigour.
This is taking taking it too far and you're placing yourself in the formalist camp, which is a minority viewpoint. You gave a nice quote from Spivak where he characterizes rigor, "...the natural medium in which to formulate and think about mathematical questions."
Labelling it a 'medium' is very informative. Computer programs likewise depend totally on the formality of the medium; it's in intrinsic part of how they are able to operate. Same with the magic of formality + inference in mathematics.
That said, the psychological questions of pedagogy involve much more than the intrinsic features of some subject. In learning to write completely formal computer programs, one benefits immensely from instruction which departs from total formality. I'm assuming this would be obvious to the readership here so I won't go into more detail.
> Completely nonsensical comparison (C++ and Haskell?? two languages who could not be further apart)
I was referring to the social standing of the languages (which is all that matters for the points I was making), not their intrinsic features.
There are reasons partly historical and partly due to the subject matter of CS that mathematicians closer to it tend to place relatively higher value on formality.
> It is also plainly true: mathematics is about rigour.
This is taking taking it too far and you're placing yourself in the formalist camp, which is a minority viewpoint. You gave a nice quote from Spivak where he characterizes rigor, "...the natural medium in which to formulate and think about mathematical questions."
Labelling it a 'medium' is very informative. Computer programs likewise depend totally on the formality of the medium; it's in intrinsic part of how they are able to operate. Same with the magic of formality + inference in mathematics.
That said, the psychological questions of pedagogy involve much more than the intrinsic features of some subject. In learning to write completely formal computer programs, one benefits immensely from instruction which departs from total formality. I'm assuming this would be obvious to the readership here so I won't go into more detail.
> Completely nonsensical comparison (C++ and Haskell?? two languages who could not be further apart)
I was referring to the social standing of the languages (which is all that matters for the points I was making), not their intrinsic features.