Removing recursion - a look into theory behind the scenes I am new to this site and this question is certainly not research level - but oh well. I have a little background in software engineering and almost none in CSTheory, but I find it attractive. To make a long story short, I would like a more detailed answer to the following if this question is acceptable on this site.

So, I know that every recursive program has an iterative analog and I kind of understand the popular explanation that is offered for it by maintaining something similar to the "system stack" and pushing environment settings like return address etc. I find this kind of handwavy. 

Being a little more concrete, I would like to (formally) see how does one prove this statement in cases where you have a function invoking chain $F_0 \rightarrow F_1 \ldots F_i \rightarrow F_{i+1} \ldots F_n \rightarrow F_0$. Further, what if there are some conditional statements which might lead an $F_i$ make a call to some $F_j$? That is, the potential function call graph has some strongly connected components.

I would like to know how can these situations be handled by let us say some recursive to iterative converter. And is the handwavy description I referred to earlier, really enough for this problem? I mean then why is it that I find removing recursion in some cases easy. In particular removing recursion from pre-order traversal of a Binary tree is really easy - its a standard interview question but removing recursion in case of post order has always been a nightmare for me. 

What I am really asking is $2$ questions

(1) Is there really a more formal (convincing?) proof that recursion can be converted to iteration?

(2) If this theory is really out there, then why is it that I find, for eg, iteratizing preorder easier and postorder so hard? (other than my limited intelligence)
You might want to look at the SECD machine. A functional language (though it could be any language) is translated into a series of instructions that manage things such as putting arguments of stacks, "invoking" new functions and so forth, all managed by a simple loop.
Recursive calls are never actually invoked. Instead, the instructions of the body of the function being called is placed on the stack to run.

A related approach is the CEK machine.

These have both been around for a long time, so there's plenty of work out there on them. And of course there are proofs that they work and the procedure for "compiling" a program into SECD instructions is linear in the size of the program (it doesn't have to think about the program).

The point of my answer is that there is an automatic procedure for doing what you want. Unfortunately, the transformation won't necessarily be in terms of things that are immediately easy for a programmer to interpret. I think the key is that when you want to iterize a program, you need to store on the stack what the program needs to do when you return from an iterized function call (this is called a continuation). For some functions (such as tail-recursive functions) the continuation is trivial. For others the continuation maybe very complex, especially if you have to encode it yourself.