Did you know that types are propositions and that programs are their proofs? You may have heard that before but have you ever wondered what it means? In this short talk, I will simply go through the proof of a very simple theorem, and show the intuitions behind the Curry-Howard isomorphism that will let us extract a program from our proof!