I could see a middle ground where one focuses attention to hardening certain parts of software systems using dependently typed languages, or proof-bearing code. The motivation just isn't there to work that hard when it doesn't matter, which is most of the time.
-----Original Message----- From: Friam <[email protected]> On Behalf Of jon zingale Sent: Wednesday, February 3, 2021 9:41 AM To: [email protected] Subject: Re: [FRIAM] coding versus music FWIW, my position is probably best summarized in an interview with Yuri Manin, where he states: "I have once translated a talk by Donald Knuth into Russian. In Uzbekistan, there was a meeting dedicated to Al'khorezmi. Knuth started his talk with a funny statement. In his opinion, the primary importance of computers for the mathematical community is that those people finally took to mathematics who were interested in mathematics but had an algorithmic sort of mind. Now they were able to do what they wanted. Before that, this subculture didn't exist. And Knuth was describing himself as a person whose mind is specially designed for writing software and how happy he was that, finally, he could do what he wanted to. I take this argument quite seriously and I do believe that among the community of future potential mathematicians there is a sub-community whose minds are better for writing computer programs than for proving theorems. In the last century, they probably would have proved theorems but nowadays they do not. I have a great suspicion that for example Euler today would spend much more of his time writing software because he spent so much of his time, e.g., in efforts of calculating tables of moon positions. And I believe that Gauss as well would spend much more time sitting in front of the screen." http://www.ega-math.narod.ru/Math/Manin.htm -- Sent from: http://friam.471366.n2.nabble.com/ - .... . -..-. . -. -.. -..-. .. ... -..-. .... . .-. . FRIAM Applied Complexity Group listserv Zoom Fridays 9:30a-12p Mtn GMT-6 bit.ly/virtualfriam un/subscribe http://redfish.com/mailman/listinfo/friam_redfish.com FRIAM-COMIC http://friam-comic.blogspot.com/ archives: http://friam.471366.n2.nabble.com/ - .... . -..-. . -. -.. -..-. .. ... -..-. .... . .-. . FRIAM Applied Complexity Group listserv Zoom Fridays 9:30a-12p Mtn GMT-6 bit.ly/virtualfriam un/subscribe http://redfish.com/mailman/listinfo/friam_redfish.com FRIAM-COMIC http://friam-comic.blogspot.com/ archives: http://friam.471366.n2.nabble.com/
