That's illuminating, thank you for a generous reply. The point about real numbers and their representation (or lack thereof) in programming languages is a great example of the gulf between mathematics and programming. I understand that for most languages, there can be no direct correspondence between a mathematical proof and the program that implements it.

In a recent discussion about the paper "How real are real numbers?" by G. J. Chaitin, someone mentioned that there seems to be a trend of a "computational" approach to mathematics on one hand, and from the other side, a "mathematization" of computer programming. With the rise of language models and their ability to generate correct programs, I imagine there is a pressing need to bridge the gulf between the two fields. Not only to verify the correctness of programs written in existing languages, but to design languages where that need for verification is taken into considertaion from the ground up, maybe close to Rust where the compiler refuses to compile a program that cannot be verified to be correct.

A common complaint about software engineering is that it is not "engineering" as a formal discipline; and about computer science that it is not a "science" (nor is it about computers, any more than astronomy is "telescope science" and biology is "microscope science" [^1]). It seems to me that a firmer grounding in mathematics, particularly in programming language design, would be helpful in improving the situation, so that software is actually "engineered" based on immutable truths and logic, and verified to be correct.

And how would the computational approach to mathematics influence it as a discipline.. Perhaps it may bring the field closer to a "science" with more experimental exploration.

[^1]: I think attributed to Vinton Cerf in _Where Is the Science in Computer Science?_. https://cacm.acm.org/opinion/where-is-the-science-in-compute...