Comment by K0nserv
10 months ago
Encoding assumptions and invariants in the type system is a spectrum. Rust, by it's very nature, places you quite far along that spectrum immediately. One should consider if the correctness achieved by this is worth the extra work. However, if there is one place where correctness is paramount, surely it's the Linux Kernel.
> [..]Attempting to do so results in code that is harder to read and write.
> You have a choice between code that statically asserts all assumptions in the type system but doesn't exist, is slow, or a pain to work with, and code that is beautiful, obvious, performant, but does contain the occasional bug.
I don't think you are expressing objective truth, this is all rather subjective. I find code that encodes many assumptions in the type system beautiful and obvious. In part this is due to familiarity, of course something like this will seem inscrutable to someone who doesn't know Rust, in the same way that C looks inscrutable to someone who doesn't know any programming.
> Encoding assumptions and invariants in the type system is a spectrum. Rust, by it's very nature, places you quite far along that spectrum immediately.
Compared to, say, dependent type systems, Rust really isn't that far along. The Linux kernel has lots of static analyzers, and then auxiliary typedefs, Sparse, and sanitizers cover a significant area of checks in an ad-hoc way. All Rust does is formalize them and bring them together.
And getting Rust into the kernel slowly, subsystem by subsystem, means that the formalization process doesn't have to be disruptive and all-or-nothing.