Almost all things you'd want to prove about a program are undecidable in the general case. That doesn't mean much about the particular case of your program.