yeah. Proving that the zero initialization is useless requires proving that the rest of the program never reads one of the zeroed values. This is really difficult because compilers generally don't track individual array indices (since you often don't even know how big the array is)