> 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...
[2] https://www.amazon.com/Turings-Cathedral-Origins-Digital-Uni...