Rust in the 6.2 kernel [LWN.net]

Rust in the 6.2 kernel

Posted Nov 19, 2022 22:45 UTC (Sat) by khim (subscriber, #9252)
In reply to: Rust in the 6.2 kernel by gasche
Parent article: Rust in the 6.2 kernel

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.

to post comments

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.