> You can have formally verified programs in a non-memory safe language. But you can't have formally verified libraries in a non-memory safe language; or rathe

> You can have formally verified programs in a non-memory safe language. But you can't have formally verified libraries in a non-memory safe language; or rather, when you use such a library in a non-memory safe language, the proofs don't carry over because the ambient program may break the underlying assumptions at any point in execution. It doesn't matter if the library carefully tracks its buffers if the main program can accidentally overwrite the library's book-keeping structures between two calls into the library.