5 ms·

> It seems unlikely that there will be any profound insights from category theory on how to write code I strongly disagree with this. To me it does not seem "

> It seems unlikely that there will be any profound insights from category theory on how to write code I strongly disagree with this. To me it does not seem "unlikely", quite the opposite. The reason I feel so strongly about this is that computer science is a subset of pure mathematics, its the part that deals with algorithms and computation. There are many questions in computer science which cannot be answered without an appeal to pure math (e.g., what is the best possible compression algorithm) All of computer science began as a result of the work of Hilbert on the foundations of logic[1]. This is what led to Turing's paper on Turing Machines. Since that time, mathematicians have done a lot of exciting work on foundations. Category theory has completely transformed the way we think about abstract mathematical objects; and type theory is very exciting in that it brings mathematics closer to a programming language which is compiled in the human brain and is done with pen and paper. It's seems to me very likely that in the future, code writing standards will change and get better, and will not remain the same. Towards that end, it makes sense that improvements will come from a better understanding of foundations, since that is where it all started. Curious for your thoughts? [1] https://en.wikipedia.org/wiki/Hilbert%27s_second_problem#:~:text=The%20system%20Hilbert%20asked%20for,than%20first%2Dorder%20Peano%20arithmetic.&text=Thus%20a%20satisfactory%20answer%20to,already%20believe%20PA%20is%20consistent https://en.wikipedia.org/wiki/Hilbert%27s_second_problem#:~:....

threatofrain 6y ago
What has been your interest in category theory? How has category theory empowered your work?
- calhoun137 6y ago
  My interest in category theory is just as a hobby and an amateur; but I have gone pretty deep reading lots of books and so on. To be fair, category theory has not empowered my work (in programming) at all.
  - feanaro 6y ago
    I find category theory empowers my programming in the design step, much more so than when actually writing code. It enables me to find a more elegant design from the outset and be sure of its utility and elegance even before I program it.
GregarianChild 6y ago
None of Zuse, Babbage, Torres y Quevedo, Ludgate, Dickinson, Desch, Atanasoff–Berry, Mauchly / Eckert, nor many of the other pioneers of computing came via Hilbert and FOM problems. An important source of early computing was the practical need for calculation (e.g. logarithm tables), leading to mechanical (and later electro mechanical) automata for automatic calculation, a tradition going back at least to ancient Greece (e.g. Antikythera mechanism). Regarding the arrow of influence: a Fields medalist spent a decade coming up with a new foundation of mathematics (or at least algebraic topology), only to realise that the computer science department already teaches Coq to undergraduates!
- calhoun137 6y ago
  > None of Zuse, Babbage, Torres y Quevedo, Ludgate, Dickinson, Desch, Atanasoff–Berry, Mauchly / Eckert, nor many of the other pioneers of computing came via Hilbert and FOM problems I don't think this is a fair comparison. The modern computer is really distinct from everything that came before. That's because it was built according to the theory of Turing Machines. One of the most important historical papers for the development of modern computers was the Report on the ENIAC by Von Neumann[1]. Von Neumann took the idea's of others working in the field, and was able to apply his understanding of mathematical logic to formulate the principles which led to the first working modern computer, which Von Neumann built in the basement of IAS. At that time, there was a major debate at IAS between Einstein and Von Neumann, which centered around whether or not to only do pure math at IAS, with the idea that building a computer was part of experimental science. [2] > Regarding the arrow of influence: a Fields medalist spent a decade coming up with a new foundation of mathematics (or at least algebraic topology), only to realise that the computer science department already teaches Coq to undergraduates! LOL! That is an interesting and funny story. However, I don't think this example demonstrates that in the future, mathematics will not be the source of improvements to code writing standards. Question: if code writing standards improve, where else will these improvements come from other than pure mathematics? I consider this question to be a problem type similar to maximum compression algorithms, i.e. its a question whose solution can only be verified using the language of pure mathematics. Therefore it seems likely these improvements can also have their roots in pure mathematics as well. At least, I would not say it "seems unlikely" [1] https://en.wikipedia.org/wiki/First_Draft_of_a_Report_on_the_EDVAC https://en.wikipedia.org/wiki/First_Draft_of_a_Report_on_the... [2] https://www.amazon.com/Turings-Cathedral-Origins-Digital-Universe/dp/1400075998 https://www.amazon.com/Turings-Cathedral-Origins-Digital-Uni...

threatofrain 6y ago

What has been your interest in category theory? How has category theory empowered your work?

calhoun137 6y ago
My interest in category theory is just as a hobby and an amateur; but I have gone pretty deep reading lots of books and so on. To be fair, category theory has not empowered my work (in programming) at all.
- feanaro 6y ago
  I find category theory empowers my programming in the design step, much more so than when actually writing code. It enables me to find a more elegant design from the outset and be sure of its utility and elegance even before I program it.

GregarianChild 6y ago

None of Zuse, Babbage, Torres y Quevedo, Ludgate, Dickinson, Desch, Atanasoff–Berry, Mauchly / Eckert, nor many of the other pioneers of computing came via Hilbert and FOM problems. An important source of early computing was the practical need for calculation (e.g. logarithm tables), leading to mechanical (and later electro mechanical) automata for automatic calculation, a tradition going back at least to ancient Greece (e.g. Antikythera mechanism). Regarding the arrow of influence: a Fields medalist spent a decade coming up with a new foundation of mathematics (or at least algebraic topology), only to realise that the computer science department already teaches Coq to undergraduates!

calhoun137 6y ago
> None of Zuse, Babbage, Torres y Quevedo, Ludgate, Dickinson, Desch, Atanasoff–Berry, Mauchly / Eckert, nor many of the other pioneers of computing came via Hilbert and FOM problems I don't think this is a fair comparison. The modern computer is really distinct from everything that came before. That's because it was built according to the theory of Turing Machines. One of the most important historical papers for the development of modern computers was the Report on the ENIAC by Von Neumann[1]. Von Neumann took the idea's of others working in the field, and was able to apply his understanding of mathematical logic to formulate the principles which led to the first working modern computer, which Von Neumann built in the basement of IAS. At that time, there was a major debate at IAS between Einstein and Von Neumann, which centered around whether or not to only do pure math at IAS, with the idea that building a computer was part of experimental science. [2] > Regarding the arrow of influence: a Fields medalist spent a decade coming up with a new foundation of mathematics (or at least algebraic topology), only to realise that the computer science department already teaches Coq to undergraduates! LOL! That is an interesting and funny story. However, I don't think this example demonstrates that in the future, mathematics will not be the source of improvements to code writing standards. Question: if code writing standards improve, where else will these improvements come from other than pure mathematics? I consider this question to be a problem type similar to maximum compression algorithms, i.e. its a question whose solution can only be verified using the language of pure mathematics. Therefore it seems likely these improvements can also have their roots in pure mathematics as well. At least, I would not say it "seems unlikely" [1] https://en.wikipedia.org/wiki/First_Draft_of_a_Report_on_the_EDVAC https://en.wikipedia.org/wiki/First_Draft_of_a_Report_on_the... [2] https://www.amazon.com/Turings-Cathedral-Origins-Digital-Universe/dp/1400075998 https://www.amazon.com/Turings-Cathedral-Origins-Digital-Uni...