101–110 of 173 posts
Earlier quoted context omitted.
> I'm not sure what it has to do with translating the code to Rust. Formally verified C programs typically have had all their undefined behaviour already stamped out during the verification process. That makes mapping it over to Rust a lot simpler.
Translating undefined behavior is the easy part.
Earlier quoted context omitted.
Translating undefined behavior is the easy part.
Maybe, but only if you know the specifics of the environment in which it is executing (i.e. which compiler/architecture-specific behaviours the code actually relies on)
Earlier quoted context omitted.
But it's not in C's standard library. So the exercise isn't merely to auto-translate one language's standard library to another language's standard library (say, replacing C++ std::list with Rust LinkedList) — which would already be very hard. The exercise here is to auto-identify-and-refactor idioms open-coded in one language, into idioms suited for the other language's already-written standard library. Imagine refa…
> The exercise here is to auto-identify-and-refactor idioms open-coded in one language, into idioms suited for the other language's already-written standard library. That's what LLMs are for - idiom translation. You can't trust them to do it right, though. [Pan et al . 2024] find that while GPT-4 generates code that is more idiomatic than C2Rust, only 61% of it is correct (i.e., compiles and produces the expected res…
https://dl.acm.org/doi/pdf/10.1145/3597503.3639226
> As for C2Rust, the 5% unsuccessful translations were due to compilation errors, the majority of them caused by unused imports.
I'm rather confused by what that's supposed to mean, since unused imports cause warnings, not errors in Rust.
Earlier quoted context omitted.
> The technology to really convert industrial-grade apps from C to Rust could probably bullet proof the C apps more easily. No, some C programs cannot be made safe. This can be due to dependency on undefined or unspecified behaviors, or it can be because introducing proper safety checks would limit the domain of possible inputs too much to be useful, or other things. Translating to a safe language can maintain the ex…
> In contrast, the Rust type system has been mathematically proven to be correct. Is this the case? E.g. the issue "Prove the Rust type system sound" https://github.com/rust-lang/rust/issues/9883 is closed with comment "This will be an open issue forever. Closing." in 2016: https://github.com/rust-lang/rust/issues/9883#issuecomment-2... . At least nowadays (since 2022) we do have a language specification for Rust: ht…
Neither of these papers include the trait system, unfortunately, and I'm not aware of another line of research that does (yet?).
Earlier quoted context omitted.
You can always run model checkers like Kani, though even that is limited.
So no?
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.)
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.
Earlier quoted context omitted.
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.)
Earlier quoted context omitted.
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
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.
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
The concept of the borrow checker has been on a simplified version of rust https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf - work has continued in this area steadily (e.g. see tree borrows)
There's a variety of tools that take rust code and translate it to something a proof system understands, and then checks that it matches a specification. AWS is leading a project to use these to verify the standard library: https://aws.amazon.com/blogs/opensource/verify-the-safety-of...
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.
What is the benefit of compiling formally correct code to Rust? It seems that all the possible benefits are already there (if not more)
Alternatively this might be seen as a stepping stone to translating non-formally-verified C to rust, which I understand the US government has expressed a fair bit of interest in.