When people talk about programming and mathematics, they're not saying that writing code should feel like high school algebra class, they're saying that mathematics is much grander than what high school put you through.
Conversation
I do think that some type checkers can provide a window into it though. Just gotta temper that with the understanding our current type checkers are limited in their ability to express the wide wonders of all that mathematics can offer.
1
AFAIK, it's also an open problem if type theory and the corresponding type checkers can every truly subsume all of mathematics, and if that is a desirable outcome for general purpose computing. I'm glad people are trying to push those boundaries though.
1
1
I think many folks get excited about mathematical structures via type systems like Haskell, which is super great. Just important to address the attrition that happens before that point, and also help people understand that these type systems only capture part of the story.