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.
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
Show replies