The one about INT_MAX is self-evident from the type system.

The one about kernel having bad types doesn't seem accurate as I checked
the source code and it uses size_t for all the appropriate types,
matching the libc struct definition for msghdr and msghdr_const.