121–130 of 173 posts
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
https://stackoverflow.com/questions/75743030/is-there-a-spec...
Earlier quoted context omitted.
> An honest title would be "Compiling a subset of F* to partially Safe Rust, Partially Formalized" Sadly that is the name of the game in conference publishing. Make a big claim in the title and hope the reviewer does not read the fine print. > If I may translate from the language of academia. "We present beautiful rules in figure 4. But in reality, our implementation relies on a large number of hacks." Er, this I can…
> Er, this I can understand. Every conference paper only presents you with a simplified view of the contributions. In my group I don't allow hacks. Most other good papers I can think of don't do that. It takes new students a while to get used to not maximizing performance at all costs. And if a hack must exist, then it's explained, not as a hack, but as part of the method. Don't you hate it when you implement some be…
Sorry if my previous comment came off as dismissive, it's just that I'm getting increasingly disillusioned with the state of things in this space.
Earlier quoted context omitted.
Is Rust formally verified? Not that I know of
Rust doesn't have a specification or standard yet, which would make it difficult to formally verify. https://stackoverflow.com/questions/75743030/is-there-a-spec...
It also strikes me as extraordinarily unlikely that any formal verification effort will use the existing specification, and not build their own (using their own formal language) as they go.
Earlier quoted context omitted.
Actually, LLMs are for generating humorous nonsense. Putting them in charge of the world economy was not intended, but we did it anyway.
Given that in my (small, employer-mandated) explorations with Copilot autocompletions it’s offered incorrect suggestions about a third of the time and seems to like to also suggest deprecated APIs, I’m skeptical about the current generation’s ability to be useful at even this small task.
If your experience with something less than half as good as state-of-the-art is that it worked 66% of the time, I am not sure why you would be so dismissive about the future potential.
Earlier quoted context omitted.
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
Then the point is hypocritical.
Runtimes for safe programming languages have been implemented in unsafe languages since the dawn of safe programming languages, basically.
EDIT: I see now that you are the cigarette warning guy. In that case I don’t understand what this coy “I think” speculation is about when you made such a bizarre proclamation on this topic.
1. Converting a C program to Rust, even if it includes unsafe code, often uncovers bugs quickly thanks to Rust’s stringent constraints (bounds checking, strict signatures, etc.).
2. automated C to Rust conversion is IMO something that will never be solved entirely, because the design of C program is fundamentally different from Rust; such conversions require a significant redesign to be made safe (of course, not all C programs are the same).
3. in some cases, it’s plain impossible to port a program from C to Rust while preserving the exact semantics, because unsafety can be inherent in the design.
That said, tooling is essential to porting, and as tools continue to evolve, the process will become more streamlined.
If you used a naïve translation to Rust, wouldn’t you get parts that are safe and parts that are unsafe? So your manual job would need to be only verifying safety in the unsafe regions (same as when writing rust to begin with)? Seems it would be a win even if the unsafe portion is quite large. Obviously not of it’s 90% of the end result.
At least it's compatible. But that approach is a dead end. To make any progress, translation must recognize the common idioms of the language and upgrade those to the ideomatic forms of the target language. Compiling into Rust generates awful Rust, full of calls to functions that do unsafe C-type pointer manipulation.
The big upgrading problems mostly involve pointers. The most promising result in this paper is that they figured out how to convert C pointer arithmetic into Rust slices. Slices can do most of the things C pointer arithmetic can do, and now someone automated the translation. Pointer arithmetic that can't be translated has to be looked at with deep suspicion.
A useful way to think about this is that raw pointers in C which point to arrays implicitly have a length associated with them. That length is not visible in C source code, but exists somewhere, as a function of the program state. It might be a constant. It might be the size requested back at a "malloc" call. It might be a parameter to a function. It's usually not too hard for maintenance programmers to find array lengths.
That could be an LLM kind of problem. Ask an LLM, "Examine this code. What is the length of array foo?" Then use that to guide translation to Rust by a non-LLM translator. If the LLM is wrong, the resulting Rust will get subscript errors or have an oversize array, but will not be unsafe. Array size info idioms are stylized enough in C that it should be possible to get it right most of the time. Especially since LLMs can read comments.
I've ported some projects to Rust (including C, where I've used C2Rust as first step), and I've drawn some conclusions. 1. Converting a C program to Rust, even if it includes unsafe code, often uncovers bugs quickly thanks to Rust’s stringent constraints (bounds checking, strict signatures, etc.). 2. automated C to Rust conversion is IMO something that will never be solved entirely, because the design of C program is…
I agree in principle, and I have strong feelings based on my experience that this is the case, but I think it would be illustrative to have some hard examples in mind. Does anyone know any simple cases to ground this discussion in?
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.
And even then, not completely reliably it seems (from Section 2.2): > The coercions introduced by conversion rules can however lead to subtle semantic differences The example they give is this C code: 1 uint8_t x[1] = { 0 }; 2 uint8_t *y = x; 3 *y = 1; 4 assert(*x == 1); /* SUCCESS */ getting translated to this (safe) Rust code: 1 let x: [u8; 1] = [0; 1]; 2 let mut y: Box = Box::new(x); 3 y[0] = 1; 4 assert!(x[0] ==…
the translated code may (quietly) not behave correctly.
If the original C program further relies on x, our translation will error out, and will ask the
programmer to fix their source code. This is another area where we adopt a “semi-active” approach
to verification, and declare that some patterns are poor enough, even for C, that they ought to be
touched up before the translation takes place.I've ported some projects to Rust (including C, where I've used C2Rust as first step), and I've drawn some conclusions. 1. Converting a C program to Rust, even if it includes unsafe code, often uncovers bugs quickly thanks to Rust’s stringent constraints (bounds checking, strict signatures, etc.). 2. automated C to Rust conversion is IMO something that will never be solved entirely, because the design of C program is…
>because unsafety can be inherent in the design I agree in principle, and I have strong feelings based on my experience that this is the case, but I think it would be illustrative to have some hard examples in mind. Does anyone know any simple cases to ground this discussion in?