3 ms·

From what I understand, it’s more like requiring each programmer to write implementations of arrays, dictionaries, date/time handling code, float parsing and pr

From what I understand, it’s more like requiring each programmer to write implementations of arrays, dictionaries, date/time handling code, float parsing and printing, etc. Once the language designers had figured out the hardware was now capable enough to make libraries useful, it only took one programmer to do that tedious work. After that all other programmers could reuse that work. This will be similar: once a large body of definitions and proofs has been built, mathematicians will be able to reuse higher-level constructs to build proofs for their theorems. It likely also will be similar in that there will be multiple approaches to this with one (or a few; it could be that one system works best/will have the largest set of definitions for one branch of mathematics, while another ‘wins’ in another) ending up victorious.

t_mann 3y ago
Exactly. There are multiple ongoing projects to formalize existing math, there seems to be some convergence on Lean4 at the moment, but the best analogy is probably programming languages, where there's a constant battle between the old guards with huge staying power and newer entrants with just too many good ideas to ignore. Except that here a lot of the attractiveness of a language will come from how much math has been formalized in that language, which gives a huge advantage to the early leaders. So there might be a bit more emphasis on 'superset-languages' like Kotlin or TypeScript here, that can make use of the libraries from existing languages.
- staunton 3y ago
  I think porting automation will eventually solve this problem. It's really easy to write "amazingly good test-suites" for this stuff. So a computer will do the porting and you essentially "only need to read mehod signatures" to make sure the port is correct. (In which case it is completely correct with all edge cases included). This is still some work but much more manageable than e.g. porting JS to Python...

t_mann 3y ago

Exactly. There are multiple ongoing projects to formalize existing math, there seems to be some convergence on Lean4 at the moment, but the best analogy is probably programming languages, where there's a constant battle between the old guards with huge staying power and newer entrants with just too many good ideas to ignore. Except that here a lot of the attractiveness of a language will come from how much math has been formalized in that language, which gives a huge advantage to the early leaders. So there might be a bit more emphasis on 'superset-languages' like Kotlin or TypeScript here, that can make use of the libraries from existing languages.

staunton 3y ago
I think porting automation will eventually solve this problem. It's really easy to write "amazingly good test-suites" for this stuff. So a computer will do the porting and you essentially "only need to read mehod signatures" to make sure the port is correct. (In which case it is completely correct with all edge cases included). This is still some work but much more manageable than e.g. porting JS to Python...