3 ms·
As a mathematician and also someone who has programmed for quite awhile I think any programmatic formalism will fail at inculcating the underlying understating.
by smohare 1y ago
As a mathematician and also someone who has programmed for quite awhile I think any programmatic formalism will fail at inculcating the underlying understating. My bias of course is that I learned mathematical concepts via academic papers.
I just feel that the overhead code presents is massive, since it often does not adhere to any semblance of style. I say say this as someone who has had to parse through other’s mathematical papers that were deemed incomprehensible. Code is 10x worse since there are virtually no standards with regards to comprehensibility.
- thdhhghgbhy 1y agoIs there not an idiomatic way to write proofs in Lean/Coq/Agda though? Idiomatic in the sense that once you learn the common idioms/tactics proofs become a degree more readable.