まだちゃんと読んでないけど、これって
「Rustでは安全に不十分なんです＞＜ やはりAda/SPARKのような形式検証を基にした発想こそが必要なんです！＞＜」
には繋げられない話なの？＞＜；