Right! That's the point of codata. If you want your program to run forever, you could express e.g. I/O events as an infinite (codata) stream. Then, instead of trying to prove that your program terminates (which it might not), it proves that your program "does something useful" every time it gets an IO event, for a particular practical definition of "doing something useful".