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