Translating All C to Rust (TRACTOR)

Think of shadow functions as the specifications that you are building. Unlike proof assistants or Frama-C, you write specifications in C itself, and they work similarly to code. Often, the same contracts you write in these specifications can be shared by both the shadow functions and the real functions they shadow.

I take a bottom-up approach to model checking. I'll start by model checking the lowest level code, then I'll shadow this code to model check code that depends on it. In this way, I can increase the level of abstraction for model checking, focusing just on the side effects and contracts of functions I shadow, and move up the stack toward more and more general code.

- Rust's compiler is 1.8 million lines of recursively compiled code, how can you or anyone know that what was written is actually trustworthy? Also memory safety is just a very small part of being able to actually trust code.

- C compiles down to straightforward assembly, almost like a direct translation, so you can at least verify that smaller programs that you write in C actually do compile down to assembly you expect, and compose those smaller programs into larger ones.

- C has valgrind and ASAN so it's at least possible to write safe code with code coding discipline, and plenty of software has been able to do this for decades.

- A lot of (almost all) higher level programming languages are written in C, which means that those languages just need to make sure they get the compiler and GC right, and then those languages can be used for general purpose, scripting, "low level" high level code like Go or OCaml, etc.

- There are many C compilers and only one Rust compiler, and it's unclear whether it'll really be feasible to have more than one Rust compiler due to the complexity of the language. So you're putting a lot of trust into a small group of people, and even if they're the most amazing, most ethical people, surely if a lot of critical infra is based on Rust they'll get targeted in some way.

- Something being open source doesn't mean it's been fully audited. We've seen all sorts of security vulnerabilities cause a world a hurt for a lot of people that came from all open source code, and often very small libraries that could actually be much easier to audit than lines with millions of lines of code.

- Similarly, Rust does not translate to straightforward assembly, and again would seem to be impossible to do given the complexity of the language.

- There was an interesting project I came across called CompCert, which aims to have a C compiler that's formally verified (in Coq) to translate into the assembly you expect. Something like a recursively compiled CompCert C -> OCaml -> Coq -> CompCert would be an interesting undertaking, which would make OCaml and Coq themselves built on formally verified code, but I'm not sure if that'll really work and I suspect it's too complicated.

- I think Rust might be able to solve some of these problems if they have a fully formally verified thing, and the formally verified thing is itself formally verified, and the compiler was verified by that thing, and then you know that you can trust the whole thing. Still, the level of complexity and the inability to at least manually audit the core of it makes me suspect it's too complicated and would still be based on trust of some sort.

- I still think that static analysis and building higher level languages on top of C is a better approach, and working on formal verification from there, because there are really small C compilers like tinycc that are ~50k LOCs, which can be hand verified. You can compile chibi-scheme with tinycc, for example, which is also about ~50k LOCs of C, and so you get a higher level language from about 100k LOCs (tcc and chibi), which is feasible for an ordinary but motivated dev to manually audit to know that it's producing sound assembly and not something wonky or sketchy. Ideally we should be building compilers and larger systems that are formally verified, but I think the core of whatever the formally verified system is has to be hand verifiable in some way in order to be trustworthy, so that you can by induction trust whatever gets built up from that, and I think that would need to require a straightforward translation into assembly, with ideally open source ISA and hardware, and a small enough codebase to be manually audited like the tinycc and chibi-scheme example I gave.

- Worst case everyone kind of shrugs it all off and just trusts all of these layers of complexity, which can be like C -> recursively compiled higher level lang -> coffeescript-like layer on top -> framework, which is apparently a thing now, and just hope that all of these layers of millions of lines of code of complexity don't explode in some weird way, intentionally or unintentionally.

- Best case of the worst case is that all of our appliances are now "smart" appliances, and then one day they just transform into robots that start chasing you around the house, all the while the Transformers cartoon theme is playing in the background while, which would match up nicely with the current trend of everything being both terrifying and hilarious in a really bizarre way.

So, they should solve total, automated testing first. Maybe in parallel. Then, use it for equivalence checks.