Compiling C to Safe Rust, Formalized

Note that this is done for “existing formally verified C codebases” which is a lot different from typical systems C code which is not formally verified.

Is Rust formally verified? Not that I know of

You can always run model checkers like Kani, though even that is limited.

So no?

The answer is that it is not.

It frustrates me more than it should, I admit, that people always mention Rust when they talk about safety, but never Ada / SPARK. You want formal verification? Use Ada / SPARK. It has been battle-tested. It has been used for critical systems for a really long time now.

(And a compiler being formally verified vs. being able to write formally verified code means two different things.)

I think a disclaimer like this should be written with every Rust application, like health warnings on cigarette packets

At this point, I think that would be better, yes, just because people think Rust is "fully" safe, which is just incorrect. I think the problem was the Rust hype and repeated statements of it being very safe, so we have some undoing to do.

For example if someone on GitHub sees that the project is written in Rust, they are automatically going to assume it is safe, incorrectly so. I do not blame them though.

You presumably extend this to every virtual machine or interpreter for every language which is implemented in an unsafe language. When that language claims to be safe (like all such languages claim to be).

That seems excessive and tedious.

The point, I think, was that "safety" presumptions about Rust are often exaggerated or poorly misunderstood due to hype. That could certainly lead to problems

I don’t think Rust’s actual safety properties aren’t overhyped, although they may be subject to misunderstanding about their exact extent.

Concretely: spatial and temporal memory safety are good things, and Rust achieves both. It’s not unique in this regard, nor is it unique in not having a formal definition.