It is well known that constructive proofs of mathematical statements implicitly contain an algorithm within them. However, actually obtaining a computer program from a formalized proof can be far from straightforward. In this talk, a constructive proof of the Fundamental Theorem of Algebra will be examined as a non trivial case study. The extracted program has many surprising properties, and it will be discussed how a careful look at this program can provide interesting insights on the process of formalization.