История изменений
Исправление hateyoufeel, (текущая версия) :
Я эти фантазии про доказательства корректности регулярно слышу, но нигде не было реальных примеров.
Чувак, ну вот свежая новость с Opennet недельной давности. На ЛОРе тоже вроде было.
https://www.opennet.ru/opennews/art.shtml?num=63104
Ты сам-то как думаешь, что такое «математическое доказательство надёжности»? Математики собрались под водовку и сказали: «слово пац^Wматематика, это надёжно!», так что ли?
Или может…
Код HACL* написан на подмножестве функционального языка F*, предлагающем систему зависимых типов и уточнений, позволяющих задавать точные спецификации (математическую модель) и гарантировать отсутствие ошибок в реализации при помощи SMT-формул и вспомогательных инструментов доказательства. Эталонный код на F* транслируется в код на языке Си при помощи компилятора KaRaMeL и доступен для интеграции с другими проектами.
Исправление hateyoufeel, :
Я эти фантазии про доказательства корректности регулярно слышу, но нигде не было реальных примеров.
Чувак, ну вот свежая новость с Opennet недельной давности. На ЛОРе тоже вроде было.
https://www.opennet.ru/opennews/art.shtml?num=63104
Ты сам-то как думаешь, что такое «математическое доказательство надёжности»? Математики собрались под водовку и сказали: «слово пац^Wматематика, это надёжно!», так что ли?
Исходная версия hateyoufeel, :
Я эти фантазии про доказательства корректности регулярно слышу, но нигде не было реальных примеров.
Чувак, ну вот свежая новость с Opennet недельной давности. На ЛОРе тоже вроде было.