Comment by jstimpfle
10 months ago
It's practically impossible to document all your assumptions in the type system. 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 am not against static safety, but there are trade offs. And types are often not the best way to achieve static safety.
> And types are often not the best way to achieve static safety.
That’s a sort of weird statement to make without reference to any particular programming language. Types are an amazing way to achieve static safety.
The question of how much safety you can reasonably achieve using types varies wildly between languages. C’s types are pretty useless for lots of reasons - like the fact that all C pointers are nullable. But moving from C to C++ to Rust to Haskell to ADA gives you ever more compile time expressivity. That type expressivity directly translates into reduced bug density. I’ve been writing rust for years, and I’m still blown away by how often my code works correctly the first time I run it. Yesterday the typescript compiler (technically esbuild) caught an infinite loop in my code at compile time. Wow!
I’d agree that every language has a sweet spot. Most languages let you do backflips in your code to get a little more control at compile time at the expense of readability. For example, C has an endless list of obscure __compiler_directives that do all sorts of things. Rust has types like NonZeroUsize - which seem like a good idea until you try it out. It’s a good idea, but the ergonomics are horrible.
But types can - and will - take you incredibly far. Structs are a large part of what separates C from assembler. And types are what separates rust from C. Like sum types. Just amazing.
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.
But if the info is info the user of your code needs in order to interface correctly, the point that you can't document everything is moot. You already have to document this in the documentation anyways.
The particular C maintainers in discussion refused to provide even textual documentation.