3 ms·

> What do you expect out of a single line? Just think of a codebase with 800k lines. Would you expect to understand what the codebase is about by just looking a

> What do you expect out of a single line? Just think of a codebase with 800k lines. Would you expect to understand what the codebase is about by just looking at a single line? The whole point is not having to understand everything at once. And I would expect to understand what that particular line does to whatever level of detail I want by reading that line and recursively working backwards through the definitions of each operation invoked. Like clicking on each identifier and then doing ‘jump to definition’ in an IDE, instead of reading a book from cover to cover. With code, I do this on a regular basis. With mathematics, it is plain impossible. (And yes, this is why literate programming is a silly idea best forgotten.) > Do you think the twin prime conjecture is still unsolved because a layperson may misinterpret the meaning of a plus sign? No. But it very much may be because too few people understand the relevant portions of number theory in sufficient depth — from the highest levels of abstraction down to the bits and bolts of set theory — to notice the key insight necessary to solve it.

xvilka 6y ago
> With code, I do this on a regular basis. With mathematics, it is plain impossible. It's easily possible with systems like Coq [1] plus a nice IDE [2]. There are mathematical libraries for the foundations [3][4]. [1] https://github.com/coq-community/awesome-coq https://github.com/coq-community/awesome-coq [2] https://github.com/coq-community/vscoq https://github.com/coq-community/vscoq [3] https://github.com/UniMath https://github.com/UniMath [4] https://github.com/math-comp https://github.com/math-comp
- pwdisswordfish2 6y ago
  That only works if someone bothered to write their proof in Coq in the first place. Most don’t.
2stop 6y ago
> The whole point is not having to understand everything at once. And I would expect to understand what that particular line does to whatever level of detail I want by reading that line and recursively working backwards through the definitions of each operation invoked. Like clicking on each identifier and then doing ‘jump to definition’ in an IDE, instead of reading a book from cover to cover. You regularly do that, using a tool built specifically to do that because it is close to impossible to read code without said tool. So are mathematicians just in need of better tooling? > (And yes, this is why literate programming is a silly idea best forgotten.) That style works pretty well for all other thought-transfer (i.e natural language)... are you sure it's a silly idea? or has the computers programmed us more than we have them?

xvilka 6y ago

> With code, I do this on a regular basis. With mathematics, it is plain impossible. It's easily possible with systems like Coq [1] plus a nice IDE [2]. There are mathematical libraries for the foundations [3][4]. [1] https://github.com/coq-community/awesome-coq https://github.com/coq-community/awesome-coq [2] https://github.com/coq-community/vscoq https://github.com/coq-community/vscoq [3] https://github.com/UniMath https://github.com/UniMath [4] https://github.com/math-comp https://github.com/math-comp

pwdisswordfish2 6y ago
That only works if someone bothered to write their proof in Coq in the first place. Most don’t.

2stop 6y ago

> The whole point is not having to understand everything at once. And I would expect to understand what that particular line does to whatever level of detail I want by reading that line and recursively working backwards through the definitions of each operation invoked. Like clicking on each identifier and then doing ‘jump to definition’ in an IDE, instead of reading a book from cover to cover. You regularly do that, using a tool built specifically to do that because it is close to impossible to read code without said tool. So are mathematicians just in need of better tooling? > (And yes, this is why literate programming is a silly idea best forgotten.) That style works pretty well for all other thought-transfer (i.e natural language)... are you sure it's a silly idea? or has the computers programmed us more than we have them?