История изменений
Исправление
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 недельной давности. На ЛОРе тоже вроде было.