The Gödel functional interpretation is a celebrated tool with a wide range of applications: consistency results, independence results, and extraction of computational content from proofs, just to name a few.