Comment by zozbot123

AIUI, proper program verification is still a very long-term goal for Rust (and most of the related short-term effort is currently going into building a formal model for the language, including its "unsafe" fragment). So, "not Rust" in that Rust simply doesn't cut it at present, whereas other solutions (Idris, Coq, even Liquid Haskell) might be closer to what's needed.