Yes but it's easy to take this too far and conclude that e.g. Javascript is not memory safe because browsers are written in C++ and they have to interface with the kernel which is written in C. At some point you simply need to trust that the current implementation is correct and bug free. This is also a problem with formal verification. What verifies the verification?