[raphlinus]

Memory safety in particular, actually UB in general (got to watch out for integer overflows, among other things). But one could prove arbitrary properties, including lack of panics (would have been helpful for a recent Cloudflare outage), etc.

In order to prove lack of UB, you have to be able to reason about other things. For example, to safely call qsort, you have to prove that the comparison is a total order. That's not easy, especially if comparing larger and more complicated structures with pointers.

And of course, proving the lack of pointer aliasing in C is extremely difficult, even more so if pointer arithmetic is employed.