In my opinion, the Curry-Howard correspondence is one of the most beautiful theoretical results, and the one that drove me to do research.

The idea that two systems, programs on the one hand, and proofs on the other hand, have exactly the same structure, is almost of philosophical nature: are there some general "reasoning patterns"?