I assume the comparison is to environments like Coq, Agda, Isabelle&#x2F;HOL, Idris, etc. But in most of those environments, there&#x27;s <i>still</i> a distinction between the language itself and the proof assistant.<p>I would not be shocked if someone figured out a brilliant way to add dependent types to Rust 1.x within the next few years.