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
On the other hand, I find doing formal proofs in Coq way more fun than I did doing proofs in college (and I enjoyed doing proofs in college). For me the supposed intuition was always a struggle and it's great to have something checking my work and every step actually justified.
1
4
Still, it's hard to get a feeling for the structure of proofs in Coq's style. Like I'll often see little ASCII diagrams showing the plan of the proof. And folks sometimes end up just randomly applying tactics without really understanding what they are doing... 🤔
1
I did that for a while (randomly applying tactics). I've found it kinda stops working once you want to do more interesting proofs.
2
Yeah, I'm still at that stage tbh. I've found the Agda-style manual proofs easier as a beginner (although I was doing them in Lean, which had less of the obscure, unpronounceable symbols).