It is well known that mathematical proofs often contain (abstract) algorithms, but although these algorithms can be understood by a human, it still takes a lot of time and effort to implement this algorithm on a computer; moreover, one runs the risk of making mistakes in the process. From a fully formalized constructive proof one can in theory automatically obtain a computer implementation of such an algorithm. As an example we consider the fundamental theorem of algebra; on the first attempts to extract a program from its formalization, the computer ran out of resources. We will discuss how we used logical techniques to extract a feasible(!) program. This example is used as a motivation for a broader perspective on how the formalization of mathematics should be done with program extraction in mind.