3 ms·
By definition, all of it. The Rust language doesn't and can't encode the semantics of, say, a DMA chip, or some other piece of hardware at some arbitrary point
by vertex-four 10y ago
By definition, all of it. The Rust language doesn't and can't encode the semantics of, say, a DMA chip, or some other piece of hardware at some arbitrary point in memory which can do arbitrary things.
Rust is built around wrapping unsafe things safely - i.e. it's possible in nearly every case to develop a performant API that doesn't let you do anything to break Rust's invariant of memory safety. Usually, these are small, meaning they're testable, which is likely good enough for almost everyone.
The next step up in safety is proving a program against a model of a system, which is a heck of a lot of hard work - you have to create a formal model of every single piece of hardware you might ever want to use. The next step after that would be proving a system actually matches the model.