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.
My point is currently programming does a poor job of opening those doors. I had more fun doing geometric proofs in middle school and physics problems in college than formally proving anything with mainstream type systems. That's why I like Shen & ATS, the flow is v. different.
3
2
Yeah, for sure. I guess maybe my misunderstanding was centered around your use of “the typechecker”. I What are your feelings about Liquid Haskell?
1
Show replies