 A further pleasing aspect of Gödel’s interpretation is that it can be extended to stronger systems such as higher order systems and even to set theory (Burr 2000, Diller 2008). Moreover, it sometimes allows one to extract computational information even from proofs of specific classical theorems (see, e.g., Kohlenbach 2007). It behaves nicely with respect to modus ponens and thus works well for ordinary proofs that are usually structured via a series of lemmata. This is in contrast to cut elimination which often requires a computationally costly transformation of proofs.