Rust in the 6.2 kernel

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.