Rust in the 6.2 kernel [LWN.net]

Rust in the 6.2 kernel

Posted Nov 19, 2022 8:56 UTC (Sat) by gasche (subscriber, #74946)
In reply to: Rust in the 6.2 kernel by ma4ris5
Parent article: Rust in the 6.2 kernel

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.

to post comments

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.