The issue isn't writes to uninitialized memory, it's reads from uninitialzed memory. The compiler doesn't know how much of the buffer `read` writes. The docs say it returns a unsigned integer with how many bytes it wrote, so a programmer can know the later read from `buffer[0..num_bytes_written]` is valid, but the compiler doesn't know what the number returned from `read` represents, so from the compiler's point of view, the whole buffer needs to be initialized regardless of what read does for reads from it to be valid. That means it has to be initialized before it's passed to read, otherwise the compiler can't prove the elements which are later read from the buffer are initialized.