I couldn't agree more. If course it would be nice of we could prove everything. It would even nicer if we would have a compiler that is smart enough. But it's just not practical for a lot of cases.