λ
есть свежий обзор, но особо про перспективу там не было, кажется -- QED at Large: A Survey of Engineering of Formally Verified Software - T. Ringer, K. Palmskog, I. Sergey, M. Gligoric, Z. Tatlock(2019)
Мог бы скинуть прям документ)
Size: a a a
2020 March 16
EM
Evgenii Moiseenko
Можно посмотреть на статьи по f*
И lean
МБ
А есть какие-то работы по этому поводу? Я часто об этом задумываюсь
Я видел только один доклад. Там было об абстрактной интерпретации. Дело было на ютубе, и я утерял ссылку. Что-то похожее делают, как я уже написал в mini kanren, но там больше о синтезе по тестам, а не о проверке. В качества апогея статья:
https://papers.nips.cc/paper/7445-neural-guided-constraint-logic-programming-for-program-synthesis.pdf
https://papers.nips.cc/paper/7445-neural-guided-constraint-logic-programming-for-program-synthesis.pdf
AT
Я видел только один доклад. Там было об абстрактной интерпретации. Дело было на ютубе, и я утерял ссылку. Что-то похожее делают, как я уже написал в mini kanren, но там больше о синтезе по тестам, а не о проверке. В качества апогея статья:
https://papers.nips.cc/paper/7445-neural-guided-constraint-logic-programming-for-program-synthesis.pdf
https://papers.nips.cc/paper/7445-neural-guided-constraint-logic-programming-for-program-synthesis.pdf
спасибо!
IJ
Вон Compcert компилируется, а ошибки в нём до сих пор находят.
Или в местах, где код неверифицирован, или в местах, где модель упрощает реальность
AT
Или в местах, где код неверифицирован, или в местах, где модель упрощает реальность
:+1:
AT
Вот и вопрос: а должен ли я заставлять своего пользователя трудиться над этим? Оно понятное дело, что дело очень интересное. Но вот есть у меня друг - биолог, ему важнее пересчитать варианты (забыл научное название) кусочков форм вирусов уже сейчас, потому как через год уже будет другой штамм гриппа...
А я вот не понимаю, есть ли вообще надежда, что когда-нибудь с типами будет легко и просто доказываться всё. А ещё лучше, будут ли завтипы выводится? Или это вообще невозможный вариант?
А я вот не понимаю, есть ли вообще надежда, что когда-нибудь с типами будет легко и просто доказываться всё. А ещё лучше, будут ли завтипы выводится? Или это вообще невозможный вариант?
Мне кажется, Вы тут немного смешиваете тёплое с мягким: (мейнстримовые) системы доказательства теорем/верификации программ - про функциаональную корректность дискретных (по сути и по факту) систем/алгоритмов, а то, чем Вы занимаетесь - больше про численную корректность (стабильность, и т.д.) непрерывных (гладких) по сути формул. Второе направление реально плохо покрыто формальной верификацией как по техническим, так и по социальным причинам.
Но "Вашего пользователя" это всё не должно волновать. Как не волнует меня как пользователя (к примеру) Scikit-learn какие именно алгоритмы и оптимизации используются в её недрах.
Но "Вашего пользователя" это всё не должно волновать. Как не волнует меня как пользователя (к примеру) Scikit-learn какие именно алгоритмы и оптимизации используются в её недрах.
IJ
Например, находили баги, связанные с допущением о бесконечности памяти, или с линковкой (а линкер еще не верифицирован). До недавнего времени доказательства писались для отдельного юнита трансляции, недавно добавилась "синтаксическая линковка" емнип
МБ
Мне кажется, Вы тут немного смешиваете тёплое с мягким: (мейнстримовые) системы доказательства теорем/верификации программ - про функциаональную корректность дискретных (по сути и по факту) систем/алгоритмов, а то, чем Вы занимаетесь - больше про численную корректность (стабильность, и т.д.) непрерывных (гладких) по сути формул. Второе направление реально плохо покрыто формальной верификацией как по техническим, так и по социальным причинам.
Но "Вашего пользователя" это всё не должно волновать. Как не волнует меня как пользователя (к примеру) Scikit-learn какие именно алгоритмы и оптимизации используются в её недрах.
Но "Вашего пользователя" это всё не должно волновать. Как не волнует меня как пользователя (к примеру) Scikit-learn какие именно алгоритмы и оптимизации используются в её недрах.
По каким социальным причинам?
IJ
Мне иногда кажется, что некоторую важную работу не выполняют не из-за отсутствия ресурсов. Такую, как формализацию экстракции из coq, например
IJ
Как с ракетами : почему мы не летим в космосе далеко ? Потому что если послать экспедицию в deep space сейчас, через 50 лет мы сделаем корабли, которые обгонят их
AT
По каким социальным причинам?
Те, кто фигачат численные алгоритмы не интересуются формальной верификацией, те, кто упарывается формальной верификацией не шарят в численных алгоритмах. 😃
AT
Те, кто фигачат численные алгоритмы не интересуются формальной верификацией, те, кто упарывается формальной верификацией не шарят в численных алгоритмах. 😃
с некоторыми исключениями вроде http://iste.co.uk/book.php?id=1238
МБ
Как с ракетами : почему мы не летим в космосе далеко ? Потому что если послать экспедицию в deep space сейчас, через 50 лет мы сделаем корабли, которые обгонят их
К сожалению, мы не летим в космос далеко, потому что энергетический потенциал современных двигателей исчерпан. Альтернатив пока нет.
Но аналогия не понятна. Какие ожидания от будущего Coq сделают эту работу не актуальной?
Но аналогия не понятна. Какие ожидания от будущего Coq сделают эту работу не актуальной?
IJ
К сожалению, мы не летим в космос далеко, потому что энергетический потенциал современных двигателей исчерпан. Альтернатив пока нет.
Но аналогия не понятна. Какие ожидания от будущего Coq сделают эту работу не актуальной?
Но аналогия не понятна. Какие ожидания от будущего Coq сделают эту работу не актуальной?
Появление новых, более эффективных техник (в аналогии двигателей)
IJ
Пруверов и тд
EZ
Как с ракетами : почему мы не летим в космосе далеко ? Потому что если послать экспедицию в deep space сейчас, через 50 лет мы сделаем корабли, которые обгонят их
Наоборот же, мы не летим в космос далеко потому что Вояджер не обогнать
IJ
Наоборот же, мы не летим в космос далеко потому что Вояджер не обогнать
В фантастике неоднократно обыгрывались ситуации, когда в глубокий космос посылались экспедиции с расчетом на успех миссии через условные 400 лет, а через 200 лет появлялись какие-нибудь технологии быстрого межзвездного путешествия, которые делали эти миссии устаревшими
EZ
В фантастике неоднократно обыгрывались ситуации, когда в глубокий космос посылались экспедиции с расчетом на успех миссии через условные 400 лет, а через 200 лет появлялись какие-нибудь технологии быстрого межзвездного путешествия, которые делали эти миссии устаревшими
А вот в жизни такого нет)
EZ
Пока что