Magical rusty thinking
> Unless this is formally proven or rewritten in a safer language...
(With the corollary that we all know there is only candidate for that "safer language" in the Linux kernel...)
Because, of course, the two are equivalent: if you write in Rust it is as good as a formal proof. Not.
Even if this guy was being hyperbolic[1] it is a bad idea to bandy around such an idea: there exist people who would love to take such an implied equivalence seriously. Without considering that, for example, memory errors of the sort Rust can deal with would be nothing compared to, say, an overly-privileged SMB server forgetting to honour any access rights[2].
Now, if there was a push from a section of the community to get code into the kernel that was written in a language amenable to formal proofs, and the accompanying proofs for each module, we could really start making some progress with a trustworthy OS[3][4]
[1] ref the mention of being paid in gold - which is a weird request but if he thinks the hassle of liquidating that is worth the hassle, each to their own
[2] no, not trying to say that KSMBD has this flaw, it is just an example of a logic/design/coding flaw that can exist without any bad memory accesses.
[3] you may say I'm a dreamer, and I'm probably the only one...
[4] btw, I'm nowhere near clever enough to create a proof of any program, let alone one worth running (I did the reading back in Uni, however...). Shameful, I know.