I think it is hard to talk about cantor diagonalization as constructive or non-constructive because it is reasoning about uncountable sets. A more down to eart

I think it is hard to talk about cantor diagonalization as constructive or non-constructive because it is reasoning about uncountable sets. A more down to earth example of a non-constructive proof would be proofs using non-constructive elements of classical logic like excluded middle (P V ~P), double negation elimination (~~P -> P) or Peirce's law (((P->Q)->P)->P). For example, this proof[1]. There are some similarities between non-constructive logic and non-purely-functional programming. It it possible to see language features such as mutable assignment, exceptions and call-with-current-continuation as analogous to the non-constructive parts of classical logic. These features all make the language depend on the order of evaluation, which destroys makes the program non-constructive[2] Anyway, I had a really good reference for this but I can't find it right now :( Hopefully someone else can provide a better link explaining how call/cc is equivalent to peirce's law. [1] http://math.stackexchange.com/a/1118851 http://math.stackexchange.com/a/1118851 [2] http://stackoverflow.com/questions/24711643 http://stackoverflow.com/questions/24711643