[sk2020]

Curiously, I’ve never seen anyone in forums take this premise to its logical conclusion and advocate the use of a language which has a much more powerful type system than Rust does, like dependent or refinement types. Haskell, Scala, Idris, and others (even Python with crosshair!) natively or with extensions support enforcing some very sophisticated constraints on a program. Tagged unions and interfaces are hardly the limit of what’s possible. However, I don’t think cutting edge type systems, theorem provers or other sophisticated tools for program validation have demonstrated enough business value to receive widespread adoption outside of only some (albeit very important) market sectors.

Really, I think most argumentation comes down to “the type system of the programming language I want to use anyway is the right one, and everything else is wrong”.