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