[ralfj]

> 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.