Comment by caim
3 days ago
Yeah, that makes sense. The Rust type system isn't "affine" as in affine logic. Rust allows different forms of contraction, which affine logic strictly prohibits.
And some people like to claim that the Curry-Howard correspondence proves something about their type system, but this is only true for dependently typed languages.
And the proofs aren't about program behavior.
> Rust allows different forms of contraction, which affine logic strictly prohibits.
That's just wrong. Affine logic totally can have contraction for some propositions.
Also, CH totally exists for non-dependently-typed languages -- for instance, there is a beautiful correspondence between the simply-typed lambda calculus and propositional logic. Please stop repeating claims that you apparently do not understand.