内容の概要><
「Ada/SPARKが好きな人から見るとRustが言う安全の範囲が都合よく独善的に見えるのは、SPARKの発想(というか形式検証の発想)から考えると当然ではあるよ」みたいな感じの英語の長文><
(超簡単に言うと、「形式検証は、安全であると証明できるものを安全と言うわけであって、メタにその発想で考えると(Rustやあるいはなんらかのよりルーズな安全性とコストバランスの線引きを行う言語が言う)安全性のスイートスポットは、その範囲の対策により安全になると証明されない限り受け入れられないだろうから、SPARKユーザーがRustを安全な環境とは見なさない事はSPARKの発想に矛盾しない」(超意訳)みたいな感じ><)