DR
Да-да, что-то такое
наверняка видел, но все же 🙂 про f* вроде шли разговоры, в тему верифицированного кодгена https://github.com/FStarLang/kremlin
Size: a a a
2020 June 10
e
наверняка видел, но все же 🙂 про f* вроде шли разговоры, в тему верифицированного кодгена https://github.com/FStarLang/kremlin
оооо фига
G
наверняка видел, но все же 🙂 про f* вроде шли разговоры, в тему верифицированного кодгена https://github.com/FStarLang/kremlin
Пока не вижу как прикрутить это к макросам
DR
ты хочешь чтобы в виде похожем на твою сишную либу генерировалось?
p
и вообще, на уровне репозитория это делается
а не снаружи
а не снаружи
Внутри репозитория возвращать IActiknResult?
e
Внутри репозитория возвращать IActiknResult?
да
G
ты хочешь чтобы в виде похожем на твою сишную либу генерировалось?
Да
DR
оооо фига
и такое есть да, там цель верифицированный tls сделать, вот этот проект https://project-everest.github.io/
e
и такое есть да, там цель верифицированный tls сделать, вот этот проект https://project-everest.github.io/
ой мля вот это реально что то полезное
G
ой мля вот это реально что то полезное
Наконец-то нашёл аргумент для срачиков, да?))
e
Наконец-то нашёл аргумент для срачиков, да?))
да :))
e
даже расширение для vscode есть. ну отлично, можно будет потыкать как нибудь
надо будет ресерч сделать, а то как будто из бункера вылез и первый раз услышал об этой штуке
надо будет ресерч сделать, а то как будто из бункера вылез и первый раз услышал об этой штуке
G
Мой совет
G
Непрошенный
G
Сначала изучи weakest precondition calculus
G
Я так и не допёр как доказывать, пока не изучил это
DR
интересно, не хочешь видеть некрасивый кодген если его как либу подключать или почему-то еще хочется именно в таком виде делать? Если прям верифицировать свой транслятор это дикий объем работы
VS
Я думал у нас все ровненько как у кабачка а оказалось пупырчато как у огурчиков(с) 😁
p
интересно, не хочешь видеть некрасивый кодген если его как либу подключать или почему-то еще хочется именно в таком виде делать? Если прям верифицировать свой транслятор это дикий объем работы
Кстати да, чтобы верифицировать по полной нужно верифицировать сначала макросы, потом верифицировать трансляцию, потом транслятор.
p
Я думал у нас все ровненько как у кабачка а оказалось пупырчато как у огурчиков(с) 😁
Ты смотришь мультик для маленьких девочек?