Rust in the 6.2 kernel [LWN.net]

Rust in the 6.2 kernel

Posted Nov 17, 2022 17:32 UTC (Thu) by khim (subscriber, #9252)
In reply to: Rust in the 6.2 kernel by atnot
Parent article: Rust in the 6.2 kernel

The difference between &str, String and Box<str> (which also) shows why Rust is a step forward while C++… not so much.

In C, of course, both “owned” and “borrowed” strings are represented as char *. C++ offers std::string and std::string_view, but… it's still responsibility of the developer to keep track of std::string_view's validity!

This makes C++ complication over C somewhat… unsatisfying: yes, we encoded difference in intents, but it's still our responsibility to keep track of everything… why do we need that complication?

But &str comes with additional assurances from the compiler: it's borrowed string, but it's compiler job to ensure that it's correctly borrowed! And String and Box<str> are owned, but it's compiler job to ensure they are correctly owned (initialized before use, etc).

That's why people say that Rust is attempting to raise the abstraction in the programming language: you genuinely can offload some of your knowledge into the machine and hope that it would verify that everything is done correctly.

It's similar to Sparse in some sense.

to post comments

Rust in the 6.2 kernel

Posted Nov 18, 2022 5:25 UTC (Fri) by ma4ris5 (guest, #151140) [Link] (5 responses)

There is some information, that Rust language is near Calculus of Constructions,
which is a bit different than Lambda Calculus.

With Calculus of Constructions, it is possible to implement logical proofs.
This would imply, that Rust implementation needs to be within the logical proofs,
for being robust.

https://www.subarctic.org/is_rust_a_purely_functional_pro...
https://hbr.github.io/Lambda-Calculus/cc-tex/cc.pdf

Rust in the 6.2 kernel

Posted Nov 19, 2022 8:56 UTC (Sat) by gasche (subscriber, #74946) [Link] (4 responses)

I know about the Calculus of Construction, and I can tell you that this is mostly wrong. There is no obvious relation between Rust and the Calculus of Construction (which is about dependent types, no linear types), and the subarctic blog you cite is wrong. This also has no relevance to the Linux kernel or string types whatsoever.

Rust in the 6.2 kernel

Posted Nov 19, 2022 15:58 UTC (Sat) by hummassa (guest, #307) [Link] (3 responses)

Your #rude filter seem to be off.
The poster was making a good point (as does the linked page) that the dependent typing usage possible using Rust traits can be used to construct purely (or semi-purely) funcional Rust programs, that can be checked via automation. The correlation to the kernel is that the same tooling possible with Rust is not possible with C++ or C.

Rust in the 6.2 kernel

Posted Nov 19, 2022 21:46 UTC (Sat) by gasche (subscriber, #74946) [Link] (2 responses)

> Your #rude filter seem to be off.

Maybe? I find it rather perplexing to see important technical ideas of our field being cargo-culted around. Why would someone name-drop the Calculus of Constructions (a rather technical topic that is mostly of experts interest) if they clearly don't know what it is? (Otherwise they couldn't claim that Rust is closely related, which is grossly wrong.) It may be that some language communities or discussion spaces are used to this kind of pseudo-technical discourse, but I'm not,
and it hurts.

(I have tried to be short and factual in my post above, which I certainly did not intend to be insulting or deprecating.)

The message I was replying can be decomposed as follows:

> There is some information, that Rust language is near Calculus of Constructions,

This information is wrong, the Rust language is nowhere near the Calculus of Constructions. Rust has a strong type system with polymorphism, sure, but that's about it (so do many other languages). The characteristic feature of the Calculus of Constructions is its very powerful pi-types / dependent abstractions, which are completely absent from Rust -- or most programming languages.

> With Calculus of Constructions, it is possible to implement logical proofs.

This is true.

> This would imply, that Rust implementation needs to be within the logical proofs,
for being robust.

I don't know what this is supposed to mean, but my best guess is that there is a fundamental misunderstanding here. Even if the Rust system *could* in theory express logical proofs (Coq or Agda can, for example), it would be entirely possible to write code that contains bugs in the language (at less precise types).

The blog post that is being cited in the message ( https://www.subarctic.org/is_rust_a_purely_functional_pro... ) is similarly fundamentally wrong. Out of the five subsections, exactly 2 are correct ("What is the Calculus of Constructions" is essentially correct, and "So is Rust purely functional" is arguably correct), the 3 other contain gross mistakes. I mean, this blog post is titled "Is Rust a Purely Functional Programming Language?", and it starts with a definition of "purely functional programming language" that is wrong?! (ML is not a purely functional programming language.)

Rust in the 6.2 kernel

Posted Nov 19, 2022 22:45 UTC (Sat) by khim (subscriber, #9252) [Link] (1 responses)

I think you are talking past each other.

> Even if the Rust system *could* in theory express logical proofs (Coq or Agda can, for example), it would be entirely possible to write code that contains bugs in the language (at less precise types).

Rust type system can express logical proofs and it's not possible to circumvent it (except for bugs in the compiler, of course). That's precisely what the Ralf's Phd thesis is about.

Now, the weird part: Rust doesn't contain full-blown dependent types system which can be used pervasively, it's complicated system is centered on lifetimes and soundness.

Which basically means that it's enough to prove that there are no UBs in safe Rust, but not enough to prove much beyond that.

That's still significantly different property from what C/C++ have. And very practically useful.

As for how all that is related to functional programming… it's, basically, impossible to say.

> it starts with a definition of "purely functional programming language" that is wrong?! (ML is not a purely functional programming language.)

Who said it's “wrong?” Even Wikipedia's article on subject start with the exact difference between pure and impure functional programming is a matter of controversy sentence for crying out loud!

The big issue here is that reasonable people define “pureness” differently and then arrive at different conclusions.

Basically the best I can say about that link is… I couldn't say if he's even right or wrong because he talks about things which have not single “proper” definition.

Rust in the 6.2 kernel

Posted Nov 20, 2022 6:28 UTC (Sun) by gasche (subscriber, #74946) [Link]

> Rust type system *can* express logical proofs

You are changing what you mean by "express logical proofs" quite a bit from what the original poster said with "implement logical proofs", quote:

> With Calculus of Constructions, it is possible to implement logical proofs. This would imply, that Rust implementation needs to be within the logical proofs, for being robust.

With the Calculus of Constructions (or other similar logics), you can define types that correspond to interesting mathematical propositions, and then you can "implement" a proof of this proposition as a program fragment at this type. This is the "Curry-Howard" view of proving things using a typed lambda-calculus, it is what the Calculus of Propositions was designed for, and this is *not* something that is done in Rust.
(Of course, as any reasonably-powerful type system, it is possible through a lot of effort to encode something similar to this process for weaker notions of propositions, using for example singleton types and what not. This does not change the fact that claiming that Rust is related to the Calculus of Constructions is fundamentally nonsensical.)

Now you are talking about a much weaker (but still important/relevant) meaning of "logical proofs", which is: proof of safety guarantees guaranteed by the type system. The idea is not that you can define types to express mathematical properties of interest, but that each type come with behavioral guarantees that gives a property that each program fragment at this type must verify. (Working out precisely how to define these guarantees is the essence of the RustBelt project and Ralf Jung's thesis.) This has, again, nothing to do with the Calculus of Constructions -- well, this work was formulated in Coq, which is maybe how the crackpots above thought to claim a connection.

> and it's not possible to circumvent it (except for bugs in the compiler, of course)

and except for, you know, *unsafe*.

> Which basically means that it's enough to prove that there are no UBs in safe Rust, but not enough to prove much beyond that.

To be fair (I'm not trying to be critical here, and your point at least are informed and make sense), you can get more than the absence of UB when you look at programs at higher type. (For example I would expect that polymorphism gives you representation-independence properties that let you reason on whether some values remain "hidden" inside a module, or what API usage patterns are prevented by the types. Some of this stuff is standard in ML/Haskell grade type systems, and there are new Rust-specific tricks that we can play with lifetimes and the static discipline.)

> Who said it's “wrong?” Even Wikipedia's article on subject start with the exact difference between pure and impure functional programming is a matter of controversy sentence for crying out loud!

There is disagreement on the finer details (and sometimes the word is used in a completely different context, "pure lambda calculus" means something else), but there is no disagreement on the fact that ML-family languages are *impure* functional programming languages; they allow for unrestricted non-termination but also mutable state, exceptions... Anyone in the field agrees that ML-family languages are *not* purely functional.

Rust in the 6.2 kernel

Posted Nov 18, 2022 16:48 UTC (Fri) by ncm (guest, #165) [Link] (4 responses)

In fact, std::string_view validity does not need to be "kept track of". Passed down a call chain, it remains valid throughout, with no phony "complication". When you need to lie to make your case, it tells us all we need to know about your case. Hype reliant on spurious denigration of other languages adds no value here.

Rust in the 6.2 kernel

Posted Nov 18, 2022 17:05 UTC (Fri) by farnz (subscriber, #17727) [Link] (3 responses)

It does need to be kept track of - you need to ensure that the underlying string is not deallocated before the string view is deallocated.

For the very specific case of just passing a string view of a string you own down a call stack, there's no issues, but as soon as the string view relates to a string whose lifespan is not determined purely by the enclosing scope (e.g. because you put the string view in a heap-allocated data structure), you have a lifespan tracking issue to worry about.

Rust in the 6.2 kernel

Posted Nov 18, 2022 18:02 UTC (Fri) by khim (subscriber, #9252) [Link]

If someone claims that use of std::string_view doesn't lead to the problems then you can safely say that it's another crop of the “just don't do any mistakes and then C works fine… oh, and don't upgrade the compiler ever because these evil guys make it break it my programs”, just with C++ theme.

Here is discussion about dangers of std::string_view on the Core Guidelines site, here is article with more arguments and there are more, but they all are, obviously, wrong, because admitting that they are right means years of investment in C++ are in jeopardy.

Just leave these guys alone. It's the same thing as with systemd introduction: there would be lots of complains and there would be holdouts and yet it would happen in the classic planck's principle way:

> An important scientific innovation rarely makes its way by gradually winning over and converting its opponents: it rarely happens that Saul becomes Paul. What does happen is that its opponents gradually die out, and that the growing generation is familiarized with the ideas from the beginning.

Rust in the 6.2 kernel

Posted Dec 12, 2022 21:04 UTC (Mon) by oconnor663 (guest, #119484) [Link] (1 responses)

You (farnz) probably already know this but I think it's worth adding: Not only deallocated, but also reallocated. Calling .push_back() or .append() on the original string also potentially invalidates a string_view.

It could be totally fair to describe these as niche issues that don't affect most callers of string_view. But I don't agree with calling someone a "liar" because you (ncm) think it's niche. Or if these issues are new to you, great! None of us is ever done learning.

Rust in the 6.2 kernel

Posted Dec 13, 2022 11:14 UTC (Tue) by farnz (subscriber, #17727) [Link]

Yes - apologies for being unclear. I think of reallocations as an optimized form of allocate, copy and deallocate, so it's implicit to me that reallocation can invalidate the original string.

At heart, this is the same problem as iterator invalidation. You have a reference to some underlying data, and changes to that underlying data can result in your reference no longer being valid. C++ has no compiler checks for reference validity, and relies on the programmer not getting it wrong; this makes some sense, since any check for reference validity is going to be conservative and thus will need overriding from time to time, but the history of "rely on the programmer not getting it wrong" suggests it's not a great decision.

Illuminating background on Rust

Posted Dec 16, 2022 12:25 UTC (Fri) by sdalley (subscriber, #18550) [Link]

That's why people say that Rust is attempting to raise the abstraction in the programming language: you genuinely can offload some of your knowledge into the machine and hope that it would verify that everything is done correctly.

Thanks khim for that very illuminating link on the functional-programming origins of Rust!