Is having the same meal two times in the same day also “cool”?
> Klint doesn't provide a way to prevent code from doing the wrong thing, it only acts a checker that things have been done right (probably). That's cool (and very useful), but quite different from e.g. "you can't make this mistake in Rust".
I don't disagree, really, but I'm trying to get a more precise idea about the distinction. Let's pretend that klint makes all the improvements listed in "future work" and all kernel developers `alias rustc=klint`. Is it any worse than the borrow checker or the type system with respect to "only [acting as] a checker that things have been done right"?
RCU does not belong in a language. Spinlocks do not belong in a language. etc. etc.
These are things that belong in libraries/modules, which leads me to think that there's absolutely zero need for a (linux) kernel specific language.
EtA: Also, while the kernel does have some mechanisms which exist elsewhere, the kernel also has its own memory model, distinct from the C++ (and eventually C) memory model, because Linux has been here a long time and needed a model before C++ had one. So this means there's a conflict between what the ISO document says (based on its memory model) and how Linux works (based on its memory model).
So it might be easier on folks if the Linux memory model wasn't just a different memory model for the C language which already has a memory model. That applies just as well for Rust.
You can't attempt sleep tokens in C or C++ because their type systems have the off-by-one error, they assume the smallest type has at least two values and requires at least one byte of storage, whereas Rust acknowledges that types might have zero or one value, and so either be unrepresentable or require no storage at all. The latter makes a sleep token possible.
This is not to deny the things that Rust does bring to the table, but it's cool to see how it cannot really address the central problem:
> How RCU is implemented in the Linux kernel lifts sleep in atomic context from "it's bad because it might cause deadlock" to "it's bad because it can cause use-after-free".
Klint doesn't provide a way to prevent code from doing the wrong thing, it only acts a checker that things have been done right (probably). That's cool (and very useful), but quite different from e.g. "you can't make this mistake in Rust".