[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Indeed, "macro" is a bad wording for translational semantics. Most effects can be explained by such a tranlation inluding continuation which are discussed here. But not all of them as e.g. various kinds of nondeterminism or probability. Also the more refined model constructions of Krivine cannot be explained this way, e.g. when he introduces a kind of quote for realizing dependent choice. But one can avoid this using bar recursion which is nothing but an instance of general recursion in the target language. This, however, does not apply to his most recent work covering full AC where he introduces extensions of lambda calculus which cannot be explained by translation to pure functional programming. As long as one does not reason about programs extracted from classical proofs it is no problem if they are cluttered with such fancy constructs. But if one does it becomes a nightmare since one does not know how to do this. That is a problem already for continuations though there exist axiomatizations for them. Therefore, the 'unwinders' rather follow the path of negative translation followed by some functional interpretation. But as soon as you go beyond Pi^0_2 the negative translation of a meaningful statement becomes fairly obscure. In any case it is very different from the original statement understood constructively. A typical example is the socalled Specker phenomenon. When you classically prove the existence of a real number then often you can extract a computable Cauchy sequence for which there does not exist a computable modulus of convergence meaning that you can't extract sufficiently good approximations. Thus, all this extraction business works only for Pi^0_2 sentences. But for those ZFC is conservative over ZF for which ordinary control operators work! Thomas