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
Yeah, for sure. I guess maybe my misunderstanding was centered around your use of “the typechecker”. I What are your feelings about Liquid Haskell?
Yeah, seems it might offer a similar experience to ATS with its liquid types. Less busy-work than in Agda and Coq (for simple stuff at least). Would like there to be a nicer gradient in languages between full proofs and solver aided stuff - but many folks are aware of that. 🙂