Maybe a bit advanced for this crowd, but there is a three-way correspondence between logic, type theory (like in programming languages), and topology. Roughly we have

Proposition ≈ Type Proof of a prop ≈ member of a Type Implication ≈ function type and ≈ Cartesian product or ≈ disjoint union true ≈ type with one element false ≈ empty type

Once you understand it, its actually really simple and “obvious”, but the fact that this exists is really really surprising imo.

You can also add topology into the mix: