I am aware, in a general sense, that the 20th century history of theoretical computer science was deeply entwined with important developments in mathematical logic and related topics in metamathematics, with topics like Church's Thesis sitting at the intersection, and with things like the Halting problem and Gödel's Theorem as, in some sense, two sides of the same coin. I imagine that such connections persist, but also that in more modern times the natural tendency toward specialization has pulled the computer science and the mathematical logic further apart than they once were.
I am wondering if someone can suggest a good reference that surveys this history, lays out some of the major connections, and sketches out the status quo vis-a-vis the relationship between computer science and mathematical logic.
There's a strong connection between Logic and Computer Science, maybe you could search for books about Computational Logic (formal specification and verification), Type Theory (natural deduction rules are very related to types, the types/classes from programming languages, this is what the Curry-Howard correspondence says), Computability Theory, Programming Languages. Logic is very important for theoretical computer science. Sorry I have no books to recommend right now covering this topics and history.