As I understand - and I may be mistaken - the problem is that it's very hard to make sure that the emitted code is correct in the presence of raw pointers à la C.

I am told that Fortran does better than C here; there is a reason it is still widely used in the scientific computing community, after all.

This is also part of the reasoning behind C99's new restrict keyword.