И это всё МОЁ
… но на самом деле не совсем. Доказана типобезопасность подмножества Rust. Соответствующая статья опубликована аж целых два года назад. А доказательство верифицировано, просто афигенский рокетсайнс.
Считаю, что об этом полезно будет узнать жителям ЛОРа, особенно некоторым анонимам.
P.S. Сам с удивлением узнал сей факт, читая наброс humbug на хабре. Очень качественный наброс, кстати. Рекомендую.