881 Кб, 611x1065Проверяем хуету, которую высрала нейронка, МАТЕМАТИЧЕСКИ.
Итт обсуждаем SAT/SMT решатели, Lean, e-graphs, TLA+, системы типов, статический анализ, Монте-Карло и подобное.
Итт обсуждаем SAT/SMT решатели, Lean, e-graphs, TLA+, системы типов, статический анализ, Монте-Карло и подобное.
>>4778 (OP)
>>4779
Практические юзкейсы есть? Как верифицировать какое-нибудь продуктовое гавнецо на тайпскрипте или питухончике которое ходит в апишки и что-то в базу данных складывает?
>>4779
Практические юзкейсы есть? Как верифицировать какое-нибудь продуктовое гавнецо на тайпскрипте или питухончике которое ходит в апишки и что-то в базу данных складывает?
>>4780
Ты проверяешь, что программа ведёт себя так, как написано в спецификации. Можно делать оптимизации AST, можно доказывать отсутствие race conditions.
>Практические юзкейсы есть?
Ты проверяешь, что программа ведёт себя так, как написано в спецификации. Можно делать оптимизации AST, можно доказывать отсутствие race conditions.
>>4778 (OP)
Что тут обсуждать? Берём ПРУВЕР, генерируем для него доказательство через ту же нейронку, запускаем, возможные ошибки тоже правим через нейронку.
Что тут обсуждать? Берём ПРУВЕР, генерируем для него доказательство через ту же нейронку, запускаем, возможные ошибки тоже правим через нейронку.
>>4781
ну вот у меня программа на питухончике - в несколько процессов ходит в апишки и потом складывает эти данные в базу.
как проверить что нет рейскондишенов? как сделать оптимизацию AST? что для этого нужно клоду написать, какой код на lean он сгенерит для этого?
ну вот у меня программа на питухончике - в несколько процессов ходит в апишки и потом складывает эти данные в базу.
как проверить что нет рейскондишенов? как сделать оптимизацию AST? что для этого нужно клоду написать, какой код на lean он сгенерит для этого?
Kukulkanos