I work as a programmer, and, outside of work, I sometimes dip into mathematical logic. My intuition alerted me to some possible connections between my job and my hobby, and I thought this might be a suitable place to sanity-check my intuition.
I was reading the other day about the distinction between first-order and higher-order logic. In higher-order logic, predicates can take other predicates as arguments; this is not allowed in first-order logic. This feels eerily similar to the situation in, say, Python, where functions can be passed to other functions as arguments, whereas in a lower-level language like C such code would not compile. Is this just a superficial similarity, or is there a deeper connection?
To come at the same question from a slightly different angle: the famous Incompleteness Theorems apply to formal systems powerful enough to express a certain level of arithmetic. That condition reminds me, in a fuzzy way, of the gear-change between Assembly and C. But, more specifically, it leads me to ask, Is is coherent to think of a programming language as a formal system within mathematical logic? If so, has anyone published anything regarding the consistency and completeness of any programming languages?