Philosophically and practically, intuitionistic type theory is a foundational framework where constructive mathematics and computer programming are, in a deep sense, the same. This point has been emphasized by (Gonthier 2008) in the paper in which he describes his proof of the Four Colour Theorem: