Владимир Ситников писал(а):
1) В репозитории "доказательств" seL4 код вообще на Haskell. Круто. Чего ж.
Нет. Дана ссылка, где проект представлен в полном виде - со статьями и полным исходным кодом. Пересказывать не вижу смысла - авторы сами хорошо постарались.
Цитата:
Те же seL4 говорят, что они предполагают идеальную работу железа. Ну, да, конечно
Вы хотели, чтобы они сотворили чудо и исправили кривое железо, а иначе не годится?
Цитата:
FDIV всегда работало верно. Иными словами, если возникает глюк железа, то всё их хвалёное доказательство трещит по швам
3) В seL4 английским по белому написано, что их "доказательство" не доказывает отсутствие timing атак. Иными словами, Spectre, Meltdown их доказательство никак не обнаруживает.
С какой стати? У них есть участок, за который они отвечают. Они его проработали. Что Вы ещё хотите, чтобы они ещё и пролёт высокоэнергетических частиц просчитали и брак на заводе учли и от сбоящей память защитили? Каким боком это относится к доказательству программ, или любым другим методам отладки? Может быть, Вы пошаговой отладкой собрались Meltdown обнаруживать?
Цитата:
4) Нужно понимать, что seL4 используют свой "доказанный" (ну или как там) компилятор.
Нет, они используют другой подход, но доказанный оптимизирующий компилятор C существует - CompCert. Впрочем, у него за рамками доказательства оказался парсер, генерируемый компилятором грамматик Menhir.
Цитата:
Понятно дело, что когда формальной верификацией покрыто 100% кода (в том числе микрокод процессоров), то это хорошо. И? Хотя бы 5% проектов находятся в таком состоянии? Море проектов, которые просто берут GCC и/или LLVM/Clang и радуются.
И что, если нам приходится использовать другое ПО, то всё - конец? Это аргумент той же силы, что "я буду курить, потому что и так дышу городским загазованным автомобилями воздухом".
Цитата:
Поймите меня правильно. Разумеется, где-то спецификация может и помочь. Но моё исходное мнение было в том, что есть много случаев, когда пошаговая отладка очень полезна.
Внимательно следите за руками. Сначала Вы утверждаете, что согласно теореме Прайса, доказывать код невозможно. Когда я указываю, что из теоремы Прайса нет такого следствия, Вы просите объяснить подробней. Сначала я показываю на простейшем примере, что код, всё-таки, в каких-то случаях можно доказывать и даю ссылки на гораздо более серьёзные учебные примеры. Затем даю ссылку на промышленное применение, так как понимаю, что это следующий этап разговора, благо раньше у людей уже возникали такие запросы. После этого Вы меняете показания и, снабжая свою речь утончённым сарказмом, начинаете писать, что, мол, доказательство корректности не умеет превращать воду в вино, не исцеляет прокажённых от болезни и, вообще, "Круто. Чего ж. Ну, да, конечно", так, как будто утверждалось обратное. Я ответил на конкретный вопрос, а не на некие домыслы, которые в итоге посыпались.
Цитата:
В той же теме я услышал "пошаговая отладка это разврат мозга на уровне импринтинга". Так там было? Ну, пусть так и будет.
У этого обсуждения есть конкретный контекст - школьная версия, образовательная система, базовые знания.
У Вас другое мнение? Я считаю это нормальным.
Цитата:
Я вижу, что вы пишете интересные штуки, но у меня совершенно нет желания, чтобы вы меня убеждали в том, что "пошаговая отладка мне не нужна".
Ещё раз, я ответил на конкретный вопрос. Я сам указывал, что пошаговая отладка может быть полезна. Вам не понравилось, что речь шла об обфусцированном коде?
Цитата:
Я понял, что вы показали как спецификация связана с реальным C кодом.
Да, это, конечно, забавнее, чем писать программу отдельно, а Coq доказательство отдельно.
Но означает ли это, что код в farma-c стиле не требует пошаговой отладки?
По-моему, не означает.
1) Например, в самой спецификации может быть ошибка. Как её обнаружить? Вдумчиво глядеть на все спецификации?
Ну, подаём в программу массив, а она один из элементов "не туда" сортирует. Ответ "работает согласно спецификации",
Как Вы себе представляете такую спецификацию?
Цитата:
3) Что, если будет ошибка в компиляторе? Ну, подаём данные на вход, а выход неверный. Спецификация на месте. Как искать ошибку?
А, Вы, наверно, думаете, что наличие доказательства отменяет тесты? Нет, спецификация - это половина информации для тестов. На "трудные" вопросы про компиляторы уже давно даны и даже стандартизированы ответы. Дмитрий Дагаев делился этими ответами касательно стандарта создания критичного ПО для АЭС. Ответы верны даже в случае аллергии на доказательства ПО.
Цитата:
4) Что, если ошибка в памяти? Ну, записывается одно значение, а читается другое. Так вам спецификация на farma-c поможет
Всё ждём воскрешения мёртвых? Ответ всё там же, у Дмитрия.
Цитата:
5) Что, если ошибка в сторонней системе? Пишете, например, клиентское приложение к PostgreSQL. Обложились спецификациями. А в реальности -- в PostgreSQL море ошибок. Как искать?
Как я уже писал, спецификации под доказательство не отменяют тесты, а наоборот - им способствуют.
Цитата:
Кстати, пользуясь случаем, предложу. У вас есть желание рассказать что-нибудь на тему тестирования, формальной верификации и т.п.
на
конференции Гейзенбаг (Москва, 6-7 декабря) для рядовых тестировщиков/разработчиков? Конференция по вопросам тестирования, и доклад на подобную тему наверняка был бы интересен.
Понимаю, что подготовка доклада это время, но вдруг интересно?
Доклад я уже делал для нужд компании, в которой работаю. Материалы для внешней конференции, наверно, нужно делать заново, но проблема не в этом. Я живу в Киеве и не люблю путешествовать. Планировать за год тоже не в моих привычках. Но спасибо за предложение.