Nah. You can deal with null-terminated strings. You "just" have to be able to prove that all operations ensure a string remains postpended with a null, and do

Nah. You can deal with null-terminated strings. You "just" have to be able to prove that all operations ensure a string remains postpended with a null, and doesn't get extended beyond the length of the underlying allocation.