SP
томака прохудился
Size: a a a
2020 June 11
e
ухахаа пздц
SP
просто пиздец и работают же люди с таким кодом
e
я так понимаю он даже форматер не юзает
если он его заюзает его простыня из fire-бола вправо сместится (либо станет нечитабельной)
если он его заюзает его простыня из fire-бола вправо сместится (либо станет нечитабельной)
SP
угу
e
и такое есть да, там цель верифицированный tls сделать, вот этот проект https://project-everest.github.io/
а есть еще какие примеры, но попроще?
что то типа вебсервера и тп
что то типа вебсервера и тп
DR
вебсервер на самом деле не особо попроще, тот же tls только часть того что есть в вебсервере
e
но что то хардово выглядит это все
e
наверное все таки F* не для таких задач использовать надо
а как раз криптография и тп
а то задолбаешься писать это все доказывать
а как раз криптография и тп
а то задолбаешься писать это все доказывать
DR
в универе показывали концепцию на примере функций сортировки, там код был на с, к нему надо было дописать специального вида аннотации на основе кокторых солвер смог бы доказать желаемое поведение
e
наверное все таки F* не для таких задач использовать надо
а как раз криптография и тп
а то задолбаешься писать это все доказывать
а как раз криптография и тп
а то задолбаешься писать это все доказывать
ну или для сабсетов кода каких-то либ
DR
примерно так выглядит
DR
наверное все таки F* не для таких задач использовать надо
а как раз криптография и тп
а то задолбаешься писать это все доказывать
а как раз криптография и тп
а то задолбаешься писать это все доказывать
верификация жутко трудоемкий процесс
DR
поэтому как раз в основном применяется для таких областей как космос и медицина
e
хах..
сразу в голову лезет мл и питон с этим
сразу в голову лезет мл и питон с этим
SP
кек
e
поэтому как раз в основном применяется для таких областей как космос и медицина
а все таки мл не в силах помочь упростить этот трудемкий процесс?
DR
ну это микропример, тулинг конечно да, не особо приятный, но свою задачу выполняет
DR
а все таки мл не в силах помочь упростить этот трудемкий процесс?
маловероятно, может быть и придумают что-то, но так сразу не видится