[marinintim]

Going to great lengths to avoid writing Rust.

[wk_end]

This is about verifying the compiler, not proving any properties of the generated code. Totally orthogonal to Rust's aims, unless the Rust compiler has been formally verified (I don't believe it has).

[strangecasts]

There has been work to verify a subset of Rust's logic - https://plv.mpi-sws.org/rustbelt/popl18/ - but the compiler itself is not verified, no.

[steveklabnik]

It has not.

[stcredzero]

Would the world be a better place if Linux, the BSD kernel behind OS X, and the Windows kernel were all rewritten in Rust? (I don't think it would be dramatically better overnight.)

[sanxiyn]

If we could do this by waving a wand without downsides (e.g. all existing maintainers magically acquire Rust knowledge, etc.), yes it would be better. No question.

Seriously, people, you can find kernel bugs at will with kernel fuzzers like syzkaller from Google. Look at https://github.com/google/syzkaller/blob/master/docs/found_b... and weep.

[AnimalMuppet]

If the Linux kernel writers all instantly knew Rust as well as they know C, then in 10 years they might produce something that is as functional as the Linux kernel currently is. In the process, they would lose everything that they could do over the next ten years to improve the Linux kernel.

You could claim that eventually the payoff would pay back the lost 10 years. But "eventually" can be a very long time...

[c1yd3i]

It would be better overnight. But it would be even better if we had one NT like kernel and a new OS built from scratch with a browser (webkit) based ui.

[stcredzero]

a new OS built from scratch with a browser (webkit) based ui

So basically, ChromeOS rewritten in Rust? Why not a Servo based UI?

[cjmaria]

The hard part is the NT-like kernel in Rust, not the web-based UI. ChromeOS uses the linux kernel.