[FrankHB]

Types are closed terms of contracts encoded in a language within specific phases. If you really need any guarantees without further knowledge shaped before running, then, besides the typechecking, the typing rules should also be programmable by users (rather than the language designer) for the sake of providing proofs. The base system must practically have no mandated static type systems at all, which is far from Rust.

[zaarn]

I would disagree, you need a solid typesystem and then any other typesystem must prove to be a compatible superset.