Well there is the Curry-Howard correspondence. Though I don't know if this correspondence is intuitive in the general case - I guess what this correspondence means is that programs can be translated to some computational model, which can then be translated to some formal logic, and then back again (but with these kinds of high-level facts, I'm bound to have misunderstood something, somewhere). Though this connection might be only intuitive for some kinds of languages - like statically typed functional languages.

I think it's amazing that programming can leverage and express so many mathematical facts - from implementing a binary tree that is enforced to always be balanced by the type system in Haskell, to using linear types to safely use and free OS resources in ATS.