>>147
when I think of how to do what you're describing, my first instinct is to run the program and collect information while I do so, but I have no way to prove that the program will terminate.
I can't really think of a way to use type-logic to determine what will happen to memory. What do you do about branching logic?