Realizability studies the computational content of proofs by defining a correspondence between the formulas of a logical system and programs in such a way that knowledge of the “realizers” (i.e. the programs associated with the formula) gives information about the proof of the formula. The Curry-Howard isomorphism establishes a correspondence between proofs of intuitionistic logic formulas and programs seen as lambda-terms. The scope of Realizability was later extended to classical logic thanks to the work by Griffin on typing operators. Thanks to Krivine, research in realizability further evolved to encompass proofs in set theory. The technique developed by Krivine generalizes the method of forcing in set theory, in fact forcing models are special cases of realizability models. This talk is meant as a gentle introduction to Forcing from the point of view of classical realizability.