We introduce the theory of formal program extraction from proofs, focusing on examples from elementary number theory. In particular, we explore the computational content of Bézout’s Lemma, the Fundamental Theorem of Elementary Number Theory, and Fermat’s Factorization. The extraction process was carried out using the proof assistant Minlog, with the resulting programs translated into Haskell code, which we will present and discuss. We will also look at the challenges that arise during formalization in Minlog and explain how the way a proof is constructed impact the efficiency of the extracted programs.