My main complaint about the math program I attended is that all of my courses felt disjoint -- they could be taken in any order, so we basically had to start over from scratch every semester, rather than allowing the material to compound over four years. I wish course selection had been more rigid.
As for teaching functional programming -- I agree with you learning category theory is not necessary for learning Haskell. But, learning Haskell is an incredibly useful and tangible way of exploring the basic ideas of category theory / type theory. I think it would be a natural addition to any math program, and the earlier students learn it the more mileage they'll get out of it. Most math programs are sorely missing a bit of computer science, anyway.
Honestly I don't find arguments that CS should be included in math programs all that convincing. What about any of the other sister fields to mathematics such as statistics or physics? I find parts of them equally compelling if not more so than CS to round out a mathematical education, but of course you quickly run out of space and time to actually include them. The crucial differentiator is that they "feel different" than normal mathematics work. I have a different set of intuitions when I'm programming in Haskell vs doing a stats problem vs doing physics. They are all deeply informed by mathematics and ultimately based on mathematics, but in each case when push comes to shove it's mathematical rigor that first goes out the window and then is hopefully later recovered rather than the other way around.
I've also never found type theory to be something useful to include at the undergraduate math level. In general, foundations of mathematics stuff is something that I think is very useful for a specific subset of undergrads who are very interested in seeing how the rigor "goes through all the way" so to speak, but for most undergrads is probably neither interesting nor useful for their future mathematical endeavors. Mathematics at large is not all that sensitive to your choice of foundations.
E.g. model theory is great! Set theory is fantastic! I have a hard time justifying their inclusion alongside the traditional three pillars of algebra, analysis, and geometry, however.
There are pedagogical reasons too. Programming has been an endless soure of applications and motivation to learn and explore math, especially computer graphics and FP. Many math students are naturally curious and explore on their own anyway, but of course a good instructor can accelerate the learning process.
Even now as a research mathematician, category theory is a good tool for guiding to the “correct” definitions of things, but virtually all the work after that is “category-less” in that it is completely and utterly specialised into the problem domain.
Category theory is still a fantastic way of organising information, stating things like universal properties, and also sometimes making “abstract nonsense” arguments (which often guide you towards some nontrivial observation in a particular category). But it is certainly not the panacea that some make it out to be.
The usual approach of teaching category theory is motivated where examples motivate the categorical gadgets, I think the unmotivated alternative (to create intuition for category theory as a formalist game) has not been explored
https://www.youtube.com/watch?v=US4Zr1WKD-8&list=PLCTMeyjMKR...
As others have stated trying to learn this abstractly first, before developing a concrete mathematical foundation, simply didn't work. I understood what the subject purported to do. I understood why I wanted to have a birds-eye view of subjects to come. The trouble is that the concepts didn't have enough to latch onto in my brain. I found myself frantically looking for examples in various subjects. In the end I realized my time was better spent in the weeds.
There's enough motivation for category theory even in basic foundations. You could start by teaching a structural set theory like ETCS as the formal counterpart of naïve set theory. Then yes, teach abstract algebra as usual but introduce category-theoretical generalizations early instead of duplicating content.
I also think that abstract algebra, linear algebra, analysis, geometry etc. even at the undergraduate level have the majority of their theorems unprovable from category theory alone.
Category theory is good for proving that the trivial is truly trivial, but the nontrivial still remains.
> Math programs should probably also start teaching Haskell or Coq in the first or second year.
I also disagree. For all the distrust many programmers have of Haskell and its "mathiness" it actually has rather little to do with mathematics and the parts that it does have to do with mathematics are generally in ways mostly irrelevant for the classical undergraduate math curriculum.
As for formal theorem provers such as Coq, though one day they may become standard mathematical rigor, that day is not now. They remain very unergonomic compared to the usual informal, but rigorous proofs in pure mathematics and often have several orders of magnitude more time to arrive at the same proof with no real increase in mathematical insight. I am personally very excited by them, but view their current status as far too premature to include in the average undergraduate mathematical curriculum.