[caim]

The main point of Affine logic is that it doesn't allow contraction, and the Rust type system does allow different forms of contraction. How exactly is Rust an "affine language"?

Also, the claims about Curry-Howard correspondence are wrong. It does not prove that rust is an affine language: https://liamoc.net/forest/loc-000S/index.xml

But Swift DOES have affine types with the "Non copyable" types that doesn't allow contraction.

[hollerith]

Rust has types that don't allow contraction, too: e.g., String, vectors and boxes.

Their being that way is essential for the borrow checker to provide the memory-safety guarantees it provides.

[caim]

Yep, that's true. But multiple immutable shared references are a form of contraction, while mutable references are actually affine.

Swift doesn't have references like Rust, and you can't even have unsafe raw pointers to variables without producing a dangling pointer, but this makes Swift more restrictive and less powerful than Rust.

[ralfj]

> multiple immutable shared references are a form of contraction

No, they are not. You're not using a value more than once, you are borrowing it, which is an extension of affine logic but keeps true to the core principles of affinity. I have modeled multiple shared references in an affine logic (look up RustBelt), i.e. in a logic that doesn't have contraction, so we have very hard evidence for this claim.

[lmm]

> The main point of Affine logic is that it doesn't allow contraction, and the Rust type system does allow different forms of contraction. How exactly is Rust an "affine language"?

The point of Affine logic is that it doesn't allow universal, unconstrained contraction, not that you can never do an operation that has the same properties that contraction would have in some circumstances. The same is true of Rust's type system.

[creata]

An affine type system is one in which some things don't have contraction, not one in which nothing has contraction.

[ralfj]

I brought up Curry-Howard to explain why I am using an SO post about "affine logic" to make an argument about the definition of "affine language". Both are defined the same way: no (universal) contraction. That claim is obviously correct, so you are going to have to be a more more concrete about which claim you disagree with.

(The other part you said about contraction and affine logics has already been successfully rebutted in some other replies so I won't repeat their points.)