“It seems unlikely that there will be any profound insights from logic on how to compute, similarly to how thousands of years of advances in the theory of numbers have had notably few implications for how to count things.“
It would be helpful if you fleshed that out a little, I'm curious about how you think insights from logic helps people program. I don't think I could deduce whether a developer knew or was ignorant of formal logic in a code review. Unless they give it away with a rather direct comment.
Recognising that a programming language is equivalent to some mathematical construct is a very different thing from getting a practical insight about what decisions to make. My shirt is some sort of topological embedded space, but the tailoring as a field has not gained much practical insight from the study of topology. Although I would encourage any aspirations the tailors have might have to a broad education.
When Faraday was asked about what the practical use of his discovery of electromagnetic induction was, he famously replied, "what is the use of a newborn baby?"
“No one has yet discovered any warlike purpose to be served by the theory of numbers or relativity, and it seems unlikely that anyone will do so for many years.”
I was referring to the fact that computers themselves are the descendants of logicians — Church, Turing, von Neumann. Your argument above could have just as easily been used to attack Turing machines before the invention of the general purpose computer.
Recognising that a programming language is equivalent to some mathematical construct is a very different thing from getting a practical insight about what decisions to make. My shirt is some sort of topological embedded space, but the tailoring as a field has not gained much practical insight from the study of topology. Although I would encourage any aspirations the tailors have might have to a broad education.