Комментарии 32
Кааак всё сложно…
Прямо открытие, что программирование -это всеголишь формальное описание задачи для вычислительной системы. Что "кодить" — это и есть "перевод с идиотского на компьютерный".
Если задача полностью формализована, то с одного формального на другой перевести сможет даже автомат.
Нужно ли использовать промежуточные "формализации на псевдоязыках"? Нужно! Если псевдоязыком владеешь лучше, чем языком программирования.
Если конечным языком владеешь достаточно хорошо для формального и точного описания задачи сразу на нём, то НЕ нужно.
Имхо, именно поэтому в первом абзаце очень чётко обозначено, что это статья не про то, как писать код — а про то, как понять — в чём проблема, как ты её собираешься решать. Спека, которую ты пишешь — это в первую очередь инструмент для обдумывания проблемы, а не способ написания конечной реализации.
А это — не очевидные вещи?
Создание "спеки" на формализованном языке НИЧЕМ не отличается от "написания конечного кода".
Чтобы рассуждать (правильно рассуждать), нужно хорошо владеть любым формальным языком — будь то язык алгебры или язык программирования.
Иногда полезно иметь "промежуточный" язык и писать на нём рассуждения. А иногда от этого больше вреда, чем пользы.
У вас на работе принята практика написания формальных спецификаций с помощью TLA+ или подобного? Вы знаете хоть кого-нибудь, у кого в российском "кровавом энтерпрайзе" принято?
Вопрос можно сделать ещё более очевидным, если спросить: сколько вообще вы знаете людей или организаций, которые хотя бы пишут тесты по-нормальному
Не пишут. Потому, что это не нужно.
Потому, что часто исходные задачи меняются быстрее, чем решаются.
Потому, что задачи такого уровня.
Тех, кому действительно нужен TLA, не нужно убеждать в том, что он нужен.
Что он из себя представляет?
Ещё один "язык высокого уровня".
Очередной "суржик" для "недоменеджеров", нихрена не смыслящих ни в программировании, ни в предметной сфере, оправдывающий лишнее звено, лишний (в 99% случаев) "слой абстракции", пожирающий ресурсы разработки.
Посудите сами, если задача полность формализована в "спеках", то "кодер"=="ручной компилятор". А если "спеки" "недоформализованы", то это фуфло, а не спеки.
А теперь объясните смысл этой работы.
Как в примерах от автора M и N переименовать в х и у?
Это, блин, что за "программисты", для которых открытие века — необходимость думать и формализовать задачи? И кто они, если им для "подумать" нужен "специальный язык"?
В спеках описывается задача и модель решения, а не конкретный способ. Более того, задача возникает при написании спеки, ведь первый этап (опять читаем статью) — определить, какой цели нужно достичь (это непросто).
то "кодер"=="ручной компилятор".
Очень хороший ручной компилятор. Намного, намного более лучший, чем просто компилятор.
Например, есть какие-то хорошо изученные темы вроде того, как по грамматике языка сгенерировать парсер. Но парсер, написанный человеком вручную почти всегда будет лучше. Не стоит недооценивать человеков :)
Хм…
Мне на почту прилетел несколько иной текст ответа.
Чтобы не было недопонимания, коротко отвечу по нему.
Так вот, я не оспариваю то, что пишет Лэмпорт в отношении "надо думать". А ещё он пишет абсолютно верную вещь, что "думать" можно на любом языке — хоть на китайском. И предлагает ОДНО ИЗ ВОЗМОЖНЫХ решений для "думать".
Я против того, чтобы это решение приподносилось как "золотая пуля" или "мастхэв" на все случаи жизни. Такое "понимание" написанного им — это и есть отрицание главного его посыла "думать надо", и пример абсолютного "клипового мышления".
Если "зомби" заставить "писать спеки", то получится "зомби, пишущий спеки".
Про "задача, возникает при написании спеков" — Вам правильно задали ниже вопрос.
А надо ли писать "спеки на спеки"? Ведь, тогда "постановку задачи" можно ещё дальше отодвинуть.
Или можно "просто думать, прежде, чем кодить"?
Я вначале отвтил в каком-то смутном состоянии духа, сорри. Потом перечитал несколько раз, понял что неправ, и исправил.
Дальше возникает вопрос: что такое постановка задачи? Допустим, если к вам приходит заказчик и говорит: вы делали мне электронный магазин еды, я хочу чтобы кнопочка "купить пожрать" теперь вела сразу на покупку, а не на корзину. Это простая, интуитивно понятная задача. Иначе говоря, с постановкой задачи справилась интуиция. (Причем совершенно не факт, что справилась правильно).
А есть какие-то другие задачи, про которые непонятно даже, в чем задача, и есть ли она здесь. А если есть — нет ни одной идеи, как ее можно решить. Может быть окажется, что чтобы только понять проблему нужно полгода времени десяти профессоров. А потом окажется, что спека есть, а решения не существует в принципе, как вам такое.
Второй вопрос, что в общем случае спека описывает не решение, а класс решений. Например, есть спецификация языка и виртуальной машины Java. А реализаций у них написана куча. Без спеки ничего такого бы не было. Причем в спеке есть такие моменты (например, вся фигня про модель памяти, многопоточность, итп), которые до конца понимают три с половиной землекопа в мире.
Мир очень разнообразная штука. Не нужно вам конкретно думать над спекой — ну не думайте, в чем проблема-то, move along citizen
Вы знаете хоть кого-нибудь, у кого в российском «кровавом энтерпрайзе» принято?
ИнфоТекс, Machine Zone Inc., T-Platforms (https://github.com/ligurio/practical-fm)
Про что конкретно?
Здравствуйте!
Если вам ещё интересно, попробуйте программу Alloy.
Она несколько отличается от TLA+.
Скажите, а за прошедшие пять лет вы пробовали что-то из этих программ?
Но, безусловно, польза от продумывания задачи перед решением огромная.
P.S. Насколько я понял, основная мысль статьи — сначала думай, потом пиши код. А чтобы убедиться, что действительно подумал — записывай.
Настоящие ведь проблемы возникают в формальной спецификации сложной предметной области.
Например, в порыве возникшего в голове алгоритма легко забыть про то же целочисленное переполнение, что может быть фатально, если мы деньги считаем или там мощность рентгена.
P.S. Если olegchir спросит автора, в чем же отличие авторского TLA+ от unit tests и напишет ответ сюда, то мы скажем спасибо.
Спросить прямо сейчас не могу, но как мне кажется разница в том, что юнит-тестирование проверяет конкретные наборы входных данных, в то время как методы формальной верификации проверяют все входные данные — это просто супер для сложных критичных систем, где можно позволить себе потратить так много ресурсов на создание действительно хорошо работающего кода.
Например, можно было бы посчитать, что действительно, TLA+ — это что-то типа продвинутого фаззера. Но фаззеру для работы нужно запустить программу множество раз, а проверяльщику модели — не нужно запускать ни разу. Он не запускает, а только проверяет. Что позволяет ему проверить бесконечное количетство запусков с бесконечным количеством шагов в каждом из них.
К примеру, в Amazon DynamoDB, TLA+ позволила обнаружить такие баги, которые требовали 35+ шагов для их воспроизведения — для этого пришлось написать спеку примерно на 1000 строк в TLA+.
Вторая идея: есть некий спектр точности написания, начинающийся формальной высокоуровневой спекой, и заканчивающийся конкретной реализацией на каком-нибудь ассемблере, и TLA+ находится где-то посередине между ними. Это такой инженерный компромисс.
Практический вывод из этого в том, что юнит-тестирование — это скорей про проверку существующей конкретной реализации, а спеки — это некоторая штука, зарисовка, с которой можно начинать думать.
Спросить прямо сейчас не могу, но как мне кажется разница в том, что юнит-тестирование проверяет конкретные наборы входных данных, в то время как методы формальной верификации проверяют все входные данные — это просто супер для сложных критичных систем, где можно позволить себе потратить так много ресурсов на создание действительно хорошо работающего кода.
Вы путаете формальную верификацию и формальные спецификации.
Формальной спецификацией называется процесс создания математически точных спецификаций, которые позволяют проанализировать дизайн системы и на этом этапе выявить часть ошибок. Формальная верификация это процесс доказательства, что программная система корректна с точки зрения требований к системе.
Вот тут можно подробнее почитать про верификацию и спецификации —
www.hillelwayne.com/post/why-dont-people-use-formal-methods
Здесь ничего не понятно. Я тоже могу сказать: чтобы стать чемпионом, тренируйтесь. Но чемпионом Вы не станете, даже если будете упахиваться на тренировках. Чтобы стать чемпионом, Вас должен тренировать чемпион, а не лузер вроде меня. И мастерство, которое тренер может показать, гораздо важнее физических нагрузок и мотивации в стиле «давай-давай, думай, пиши спецификацию». Мастерства в статье и нет. Статья ни о чем. В раздел «мотивация» ее нужно отправить.
Заминусуют — ну и плевать.
Ни одного внятного примера спецификаций не приведено.
Примеры лучше посмотреть в лекциях самого автора или на сайте learntla.com.
Но везде где я работал, все пытаются спихнуть задачи бизнеса на программистов тоже, а спека получалась не спекой, а описанием бизнеса, не более.
Пойду, наверное, убиваться об стенку. Ведь я недопрограммист, судя по заявленному я, получается, один из «нелюбителей тестировать написанное».
Или, все-же, тестировать «написанное» должен автор?
Добрый день!
Скажите, а вы пробовали Alloy?
Вы лично пишете спецификации?
Мне интересен любой опыт их применения в России.
Программирование — больше, чем кодинг