Compiling C to Safe Rust, Formalized

What is the main difference? Can compiler flags force compliance?

Formal verification often requires simplified code in a restrictive style. You might not even be able to use C features or structures that have the performance you want. How theorem provers and brains work are also different enough that making something easy for one often makes it harder for the other.

You can also see this effect in the article on the history of Coverity’s analyzer. Real-world code was horrible to deal with vs the academic examples they started with.

https://cacm.acm.org/research/a-few-billion-lines-of-code-la...

My understanding is that formal verification is a tough goal to achieve and that it usually requires designing the program or the language to be a specific way.

The problem with transpiling C to rust is that unsafe and unverified behavior can be a key property of the behavior resulting program, so there isn’t an obvious way to spit out a sort of rustified (CRustified?) binary that matches the behavior of the C program.

Typical term is “Oxidized”. I think they feel clever when they do the RiiR thing and say that.

"Formally verified" means someone has written a correct mathematical proof that the code has no bugs (the proof is checked by a computer program to make sure it is correct). This is a very high bar.

I'm not sure what it has to do with translating the code to Rust.

> 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.

In this case specifically, two separate aspects are being referred to with regard to "formal verification".

The first is that the translation function (from C to Rust) has itself been formally verified. In other words: if you give it a C program that obeys certain necessary pre-conditions, it will give you a safe Rust program. I believe the title of the paper is primarily using "Formalized" with regard to this characteristic.

The second is that the set of programs the authors evaluate their tool on are C programs that have themselves been formally verified. I only barely skimmed the introduction and didn't see it addressed directly there, but I would assume that this is because the pre-conditions necessary for their translation to work are most easily (only?) met by formally verified C programs, where of course the verification has been rendered with respect to properties that would be relevant here (e.g., memory use).

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)

Correctly written C programs don’t have undefined behaviour, so a translator can operate assuming there is none.

> "Formally verified" means someone has written a correct mathematical proof that the code has no bugs

No, only that it complies with a formal specification. The code will have bugs if and only if the specification has bugs.

The difficulty of writing a bug-free formal specification is just as great as writing bug-free code. In some domains it's easier to write the specification, but not in most. Fully specifying what a program shoud do is often the hardest part of programming, after all.