I have plans slated for doing proofs about Rust programs in 2017, if not sooner (I'm interning at Data61 on the seL4 verification team starting in two weeks, and if I don't get a chance to work on Rust verification then, I'll start after I'm done)

Oh hell, you going to be working with the top talent. You might learn some high assurance skills after all. That makes your project 2x as interesting. Good luck on the new job. :)

Rust has long been capable of running without a runtime (that's how all OS development in Rust is expected to operate) and formal verification of the language spec is ongoing (though full verification is still probably years out, and who knows if the compiler will ever be formally verified).

Hell yeah! Appreciate the updates. My idea there was a runtime or overhead came from an early OS attempt in Rust where they couldnt get past real mode. Had to use non-Rust code for that and it was using too much space IIRC. They've gotten past those obstacles now?

You need about 100 lines of assembly to get to a Rust kmain in long mode.

Rust has effectively no runtime these days. Same amount as C or C++, basically.

That's great to hear. Thanks for chiming in with the good info as always.

Any time. If you're interested in what exactly that code is, check out Phil's blog, linked upthread.

I'm guessing you mean this:

http://os.phil-opp.com/entering-longmode.html

Interesting stuff and seems like a good description of the code. Bookmarking it in case I do more in this area.