Sorry, I think I had misinterpreted your point. So you're saying that there are only 2 options: 1. You either simulate running the program step-by-step (which

Sorry, I think I had misinterpreted your point. So you're saying that there are only 2 options: 1. You either simulate running the program step-by-step (which has an extreme time complexity problem). 2. Or, you try to analyze it within some system of logic. But if you do so, then there are things that you can't prove because logic itself can't prove certain statements. This is an interesting argument. But I think point 1 sort of disproves point 2. Point 1 means that you can always analyze such programs, it's just that it might take a really long time to achieve that. So I think point 2 is not valid in this specific context. Because you can always prove whatever you want (given that when you simulate running a program, you are necessarily doing it within a system of logic), it's just that we don't know how long that could take in theory (of course, in practice, it's currently intractable). So if you can always prove whatever you want, that means Godel's results about the undecidability of certain statements don't apply when analyzing finite-state computation systems, only infinite ones.