![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Прочитал интересную серию статей Paul Callaghan в PragPub (https://pragprog.com/magazines, выпуски с 38 по 49, кроме 44, а существенная для этого текста часть — с 45-го), и сделал для себя некий существенный вывод, к которому эта серия — прекрасная иллюстрация. Оным выводом и хочу поделиться.
Раз мы говорим "оптимальный", то встают вопросы "по какому критерию?" и "при каких краевых условиях?" У меня пока не получается четко разделить. Краевым условие точно будет "достаточно надежная программа", а вот критерием оптимальности оказывается неочевидная комбинация из затрат времени и внимания на ее написание или модификацию (модификация через год-два — это важно) и степени моей уверенности в том, что программа достаточно надежна. Собственно, одна из умных мыслей, явно сформулированных Каллаганом — это как раз про степень уверенности.
Как нетрудно догадаться, даже краевое условие весьма размытое и для разных проектов различно, не говоря уже о критерии оптимальности. Я бы с удовольствием перевел степень уверенности в разряд краевых условий, чтобы измерять только время (для достижения заданной степени уверенности), тогда можно было бы померить, но... на практике время тоже лимитировано, и если за это время не удается достичь желаемой уверенности, полученная уверенность окажется ниже желаемой. Возможно, существенно ниже. Здравствуй, невроз.
Сразу озвучу совсем уж сухой остаток. На данный момент развитие средств программирования таково, что оптимум называется Haskell. Может быть, еще какие-то сходные языки, не уверен. Ключевые моменты: богатая система типов и статическая их проверка. Только вместе. Но. Более богатые, чем хаскель, средства (зависимые типы) пока оказываются намного ниже оптимума.
Для меня несколько лет назад хаскель оказался большим скачком вперед в рассматриваемой схеме по сравнению со всем, что я видел до этого. В первую очередь по критерию уверенности. Выразительная сила у него сравнима с выразительной силой современных ОО-языков, особенно динамических. А вот по уверенности в правильной работе результата хаскель их оставляет далеко позади.
За четыре года работы на хаскеле над достаточно большой, сложной и довольно плохо поставленной задачей (несколько радикальных переосмыслений ситуации, несколько крупных рефакторингов кода) через компилятор успешно прорвалось меньше десятка ошибок, из которых только одна по своей природе отличалась от "перепутал знак в формуле или ветки в if". И эта одна не ловилась бы никакими тестами. Как черный ящик там все работало, только память текла. Не очень сильно причем. Может, на нее никто никогда бы не наступил, тренажеры все же регулярно обесточивают. Остальные моментально ловились ручным тестированием. Ни одного автоматизированного теста у программы нет. Ни одной ошибки, которую они могли бы поймать, а минимальное ручное тестирование не поймало, в процессе эксплуатации обнаружено не было. Даже ошибок вида "сложили градусы с радианами", применяя хаскель, вполне можно избежать. Причем не путем запрета, а путем автомагического преобразования. Пакет dimensional, кто понимает.
Параллельно мне пришлось делать сайт. Я выбрал в качестве движка Ruby on Rails. Ну, так получилось... Сайт вроде работает, и трогать его я боюсь. А поскольку он требует крупного рефакторинга (рефакторинг модели бизнес-процесса, для сайта это даже рефакторингом уже назвать нельзя, на уровне программы функциональность меняется), то сейчас я взялся переделывать его на хаскель (движок yesod), чтобы не бояться трогать. Рельсы, конечно, лучше развиты в плане готового, но без дикого количества тестов трогать такой продукт не стоит. Проверено, мин есть. А автоматизированное тестирование веб-сайта, особенно с жабоскриптами — сами понимаете...
Небо и земля. То есть дойти до хаскеля точно стоит.
А дальше? Опять же параллельно, один коллега, несколько разочаровавшись в хаскеле как в серебряной пуле, потыкался в Agda. И даже написал на ней программу. И она даже работает. Но тоже серебряной пули не нашел. Я тоже краем глаза глянул, но писать программы не пробовал. А вот Каллаган в своей статье попробовал... Теперь — иллюстрация.
Интересующая меня в этом тексте часть начинается с того, что он берет учебную задачу, весьма простую, но уже не вполне тривиальную. Дан текст в виде строки, надо его разбить на строки не больше заданной длины, понятно, забивая каждую строку по возможности до упора. Если какое-то слово оказывается длиннее, его надо порезать, а если влезает, то не надо.
Поскольку задача пришла несколько снаружи, из серии постов другого человека, большого специалиста по tests-driven development, то Каллаган начал с TDD-подхода. Получил код из 11 строк, который успешно проходил все 6 исходных тестов, но был коряв и содержал слегка замаскированную ошибку, которую он сам быстро поймал ручным тестированием и добавил седьмой тест. Впрочем, в этом коде он потом нашел еще одну ошибку.
Каллаган не заострял на этом внимания, а я заострю. Набор тестов, предложенных большим специалистом по TDD, оказался плохим сходу. Развивая наблюдение дальше, можно сделать вывод, что TDD, пока набор тестов вменяемого размера, дает очень плохую уверенность. Кто работал со мной в Криптокоме, тот помнит, какой у нас был объем тестов, дававший пристойную уверенность, и сколько времени занимал их прогон. Коллеги в Транзасе рассказывали, что когда они ввели в работу Smalltalk, поначалу у них, как положено, был набор автоматизированных тестов на основной код тренажера. Все равно недостаточный, но вскоре его прогон начал занимать столько времени, что все стали отключать запуск тестов. И уже много лет этот код не тестируется, на него дышать боятся, и тем не менее, периодически ломают. Починить сломанное обычно может ровно один человек в отделе. Остальные — в лучшем случае не сломать.
Окей, говорит Каллаган, что-то мне этот код самому тоже не нравится. Давайте попробуем функциональный подход к задаче, а тесты будем использовать для проверки, а не для драйва :) Функциональный подход он, кстати (это другая весьма интересная мысль) определил как подход "от данных". Помните "алгоритмы + структуры данных = программы", что считается краткой формулировкой процедурного подхода и отвергнуто объектно-ориентированными гражданами? Тут акцент смещен: структуры данных плюс их обработка.
Функциональный подход дал ему очень хороший результат, причем даже без введения типов, специфичных для задачи — вполне библиотечных строк и списков строк ему хватило. Получился код на 16 строк, если расписывать его экстремально развесисто, и на 9, если по-человечески, по которому за минуту его внимательного видно, что он работает правильно. Из этих 9 строк 7 — кастомная функция слияния фрагментов слов в строку до заданной длины (три ветки выполнения, рекурсия и одно вспомогательное определение). Остальные две — совершенно очевидные пайпы из простейших библиотечных функций обработки списков и строк. Возможно, кастомную функцию тоже можно сформулировать как foldr, но вряд ли она от этого станет более внятной.
Опять заострю внимание. Тесты эта программа проходит, но они ей, по крайней мере эти, тупо не нужны. Чтение кода дает на порядок больше уверенности в ее правильной работе, чем эти тесты.
А вот дальше — самое интересное. Иллюстрация к тому, что дальше оптимум пройден.
Система проверки типов хаскеля, говорит Каллаган, не может проверить нам ряд свойств этой программы, в которых мы хотели бы быть уверены — например, что результирующие строки действительно не будут длиннее, чем велели, или что программа не переставляет ничего в тексте, только делит его на строки (первой ошибкой, которую не ловили исходные тесты, у него был забытый в одном из двух мест reverse — довольно частая ошибка у начинающих программистов на хаскеле). Мы, конечно, можем поразмахивать руками, но давайте попробуем получить больше уверенности гарантированно. И берет Idris — систему с зависимыми типами.
Тут-то мне и стало особенно интересно. Потому что демонстрация прелестей зависимых типов обычно не идет дальше безопасного head. Кто программировал на хаскеле, тот знает, что библиотечные head и tail выкидывают ошибку времени выполнения, если входной список пуст. Весьма жесткую ошибку, они считаются аналогами Null Pointer Exception для хаскеля. Причем если tail еще мог бы как-то выкрутиться, то head не может никак — у него тип
А на самом деле система с зависимыми типами — это всегда система с доказательством программы. "Программа успешно скомпилировалась" в них означает "мы доказали про нашу программу некоторые свойства, выраженные в ее типе". См. соответствие Карри-Ховарда. Доказали строго — так, что нам поверила машина. А она рукомашеству не верит.
Хаскель, на самом деле, тоже проверяет доказательство. Поскольку соответствие Карри-Ховарда. Только у хаскеля, во-первых, выразительные возможности системы типов бедноваты, а во-вторых, есть unsafePerformIO :)
Каллаган, как честный ежик, попытался решить на Idris ту же задачу. Очень простую, но не вполне тривиальную. И...
Свойство "ничего в тексте не переставляет" он, похоже, даже сформулировать за 4 месяца не осилил. Доказать свойство про длину очевидного, понятного с первого прочтения, хаскельного кода — тоже. Сформулировать осилил, а доказать — уже нет.
Дальше он попытался написать программу иначе, так, чтобы справиться с доказательством. Что, в общем, не бессмысленно — как тупой перевод на хаскель программы с Java возможен, но не полезен для нервного здоровья, так и тут было бы вполне логично, если правильный способ писать программу на Idris отличается от такового на Haskell.
Легкая часть (деление слов на фрагменты) у него заняла больше 30 строк, и я не могу сказать, что из аннотаций типов мне очевидно, что она обладает заявленными свойствами. Т.е. она вроде проходит тайп-чекер (сам я не проверял), но мне совершенно не очевиден тот факт, что тот тип, которому соответствует код, выражает именно то свойство, которое должен по замыслу автора. Тяжелую часть он обещал дочистить и выложить на гитхаб. Обещал в июле 2013 г. Я туда сходил. Там до сих пор placeholder. Не осилил, похоже.
И это человек с бэкграундом в виде написания пруфчекера.
Отсель мораль. Затраты на получение бОльшей уверенности, чем предоставляет хаскель — астрономические. Если вы пишете софт, который будет работать автономно в дальнем конце Солнечной системы лет через 20 после запуска, то они могут окупиться. Тогда собирайте команду ОЧЕНЬ хороших программистов с ОЧЕНЬ хорошим математическим бэкграундом, берите заказ у NASA лет на 10 работы (не одного человека а всей команды), пишите очевидный код, и упирайтесь его доказывать. Не пытайтесь писать код, который будет легче скормить пруфчекеру, но который будет не очевиден — это тупиковый путь.
Может быть, дальше средства доказуемого программирования разовьются и будет лучше. Но пока, если вы хотите уверенности в надежности своей программы за вменяемое время, оптимум называется Haskell.
Раз мы говорим "оптимальный", то встают вопросы "по какому критерию?" и "при каких краевых условиях?" У меня пока не получается четко разделить. Краевым условие точно будет "достаточно надежная программа", а вот критерием оптимальности оказывается неочевидная комбинация из затрат времени и внимания на ее написание или модификацию (модификация через год-два — это важно) и степени моей уверенности в том, что программа достаточно надежна. Собственно, одна из умных мыслей, явно сформулированных Каллаганом — это как раз про степень уверенности.
Как нетрудно догадаться, даже краевое условие весьма размытое и для разных проектов различно, не говоря уже о критерии оптимальности. Я бы с удовольствием перевел степень уверенности в разряд краевых условий, чтобы измерять только время (для достижения заданной степени уверенности), тогда можно было бы померить, но... на практике время тоже лимитировано, и если за это время не удается достичь желаемой уверенности, полученная уверенность окажется ниже желаемой. Возможно, существенно ниже. Здравствуй, невроз.
Сразу озвучу совсем уж сухой остаток. На данный момент развитие средств программирования таково, что оптимум называется Haskell. Может быть, еще какие-то сходные языки, не уверен. Ключевые моменты: богатая система типов и статическая их проверка. Только вместе. Но. Более богатые, чем хаскель, средства (зависимые типы) пока оказываются намного ниже оптимума.
Для меня несколько лет назад хаскель оказался большим скачком вперед в рассматриваемой схеме по сравнению со всем, что я видел до этого. В первую очередь по критерию уверенности. Выразительная сила у него сравнима с выразительной силой современных ОО-языков, особенно динамических. А вот по уверенности в правильной работе результата хаскель их оставляет далеко позади.
За четыре года работы на хаскеле над достаточно большой, сложной и довольно плохо поставленной задачей (несколько радикальных переосмыслений ситуации, несколько крупных рефакторингов кода) через компилятор успешно прорвалось меньше десятка ошибок, из которых только одна по своей природе отличалась от "перепутал знак в формуле или ветки в if". И эта одна не ловилась бы никакими тестами. Как черный ящик там все работало, только память текла. Не очень сильно причем. Может, на нее никто никогда бы не наступил, тренажеры все же регулярно обесточивают. Остальные моментально ловились ручным тестированием. Ни одного автоматизированного теста у программы нет. Ни одной ошибки, которую они могли бы поймать, а минимальное ручное тестирование не поймало, в процессе эксплуатации обнаружено не было. Даже ошибок вида "сложили градусы с радианами", применяя хаскель, вполне можно избежать. Причем не путем запрета, а путем автомагического преобразования. Пакет dimensional, кто понимает.
Параллельно мне пришлось делать сайт. Я выбрал в качестве движка Ruby on Rails. Ну, так получилось... Сайт вроде работает, и трогать его я боюсь. А поскольку он требует крупного рефакторинга (рефакторинг модели бизнес-процесса, для сайта это даже рефакторингом уже назвать нельзя, на уровне программы функциональность меняется), то сейчас я взялся переделывать его на хаскель (движок yesod), чтобы не бояться трогать. Рельсы, конечно, лучше развиты в плане готового, но без дикого количества тестов трогать такой продукт не стоит. Проверено, мин есть. А автоматизированное тестирование веб-сайта, особенно с жабоскриптами — сами понимаете...
Небо и земля. То есть дойти до хаскеля точно стоит.
А дальше? Опять же параллельно, один коллега, несколько разочаровавшись в хаскеле как в серебряной пуле, потыкался в Agda. И даже написал на ней программу. И она даже работает. Но тоже серебряной пули не нашел. Я тоже краем глаза глянул, но писать программы не пробовал. А вот Каллаган в своей статье попробовал... Теперь — иллюстрация.
Интересующая меня в этом тексте часть начинается с того, что он берет учебную задачу, весьма простую, но уже не вполне тривиальную. Дан текст в виде строки, надо его разбить на строки не больше заданной длины, понятно, забивая каждую строку по возможности до упора. Если какое-то слово оказывается длиннее, его надо порезать, а если влезает, то не надо.
Поскольку задача пришла несколько снаружи, из серии постов другого человека, большого специалиста по tests-driven development, то Каллаган начал с TDD-подхода. Получил код из 11 строк, который успешно проходил все 6 исходных тестов, но был коряв и содержал слегка замаскированную ошибку, которую он сам быстро поймал ручным тестированием и добавил седьмой тест. Впрочем, в этом коде он потом нашел еще одну ошибку.
Каллаган не заострял на этом внимания, а я заострю. Набор тестов, предложенных большим специалистом по TDD, оказался плохим сходу. Развивая наблюдение дальше, можно сделать вывод, что TDD, пока набор тестов вменяемого размера, дает очень плохую уверенность. Кто работал со мной в Криптокоме, тот помнит, какой у нас был объем тестов, дававший пристойную уверенность, и сколько времени занимал их прогон. Коллеги в Транзасе рассказывали, что когда они ввели в работу Smalltalk, поначалу у них, как положено, был набор автоматизированных тестов на основной код тренажера. Все равно недостаточный, но вскоре его прогон начал занимать столько времени, что все стали отключать запуск тестов. И уже много лет этот код не тестируется, на него дышать боятся, и тем не менее, периодически ломают. Починить сломанное обычно может ровно один человек в отделе. Остальные — в лучшем случае не сломать.
Окей, говорит Каллаган, что-то мне этот код самому тоже не нравится. Давайте попробуем функциональный подход к задаче, а тесты будем использовать для проверки, а не для драйва :) Функциональный подход он, кстати (это другая весьма интересная мысль) определил как подход "от данных". Помните "алгоритмы + структуры данных = программы", что считается краткой формулировкой процедурного подхода и отвергнуто объектно-ориентированными гражданами? Тут акцент смещен: структуры данных плюс их обработка.
Функциональный подход дал ему очень хороший результат, причем даже без введения типов, специфичных для задачи — вполне библиотечных строк и списков строк ему хватило. Получился код на 16 строк, если расписывать его экстремально развесисто, и на 9, если по-человечески, по которому за минуту его внимательного видно, что он работает правильно. Из этих 9 строк 7 — кастомная функция слияния фрагментов слов в строку до заданной длины (три ветки выполнения, рекурсия и одно вспомогательное определение). Остальные две — совершенно очевидные пайпы из простейших библиотечных функций обработки списков и строк. Возможно, кастомную функцию тоже можно сформулировать как foldr, но вряд ли она от этого станет более внятной.
Опять заострю внимание. Тесты эта программа проходит, но они ей, по крайней мере эти, тупо не нужны. Чтение кода дает на порядок больше уверенности в ее правильной работе, чем эти тесты.
А вот дальше — самое интересное. Иллюстрация к тому, что дальше оптимум пройден.
Система проверки типов хаскеля, говорит Каллаган, не может проверить нам ряд свойств этой программы, в которых мы хотели бы быть уверены — например, что результирующие строки действительно не будут длиннее, чем велели, или что программа не переставляет ничего в тексте, только делит его на строки (первой ошибкой, которую не ловили исходные тесты, у него был забытый в одном из двух мест reverse — довольно частая ошибка у начинающих программистов на хаскеле). Мы, конечно, можем поразмахивать руками, но давайте попробуем получить больше уверенности гарантированно. И берет Idris — систему с зависимыми типами.
Тут-то мне и стало особенно интересно. Потому что демонстрация прелестей зависимых типов обычно не идет дальше безопасного head. Кто программировал на хаскеле, тот знает, что библиотечные head и tail выкидывают ошибку времени выполнения, если входной список пуст. Весьма жесткую ошибку, они считаются аналогами Null Pointer Exception для хаскеля. Причем если tail еще мог бы как-то выкрутиться, то head не может никак — у него тип
[a] -> a, и если список пуст, ему валидное значение для возврата тупо неоткуда взять. Так вот, демонстрация зависимых типов начинается (и заканчивается) определением семейства векторов конечной длины, которые на уровне проверки типов (т.е. времени компиляции, а не выполнения) имеют известную длину, и определением head таким образом, что он работает только на векторах длины на 1 больше некоторой другой длины. На потенциально бесконечных списках и списках неизвестной длины — не могут.А на самом деле система с зависимыми типами — это всегда система с доказательством программы. "Программа успешно скомпилировалась" в них означает "мы доказали про нашу программу некоторые свойства, выраженные в ее типе". См. соответствие Карри-Ховарда. Доказали строго — так, что нам поверила машина. А она рукомашеству не верит.
Хаскель, на самом деле, тоже проверяет доказательство. Поскольку соответствие Карри-Ховарда. Только у хаскеля, во-первых, выразительные возможности системы типов бедноваты, а во-вторых, есть unsafePerformIO :)
Каллаган, как честный ежик, попытался решить на Idris ту же задачу. Очень простую, но не вполне тривиальную. И...
Свойство "ничего в тексте не переставляет" он, похоже, даже сформулировать за 4 месяца не осилил. Доказать свойство про длину очевидного, понятного с первого прочтения, хаскельного кода — тоже. Сформулировать осилил, а доказать — уже нет.
Дальше он попытался написать программу иначе, так, чтобы справиться с доказательством. Что, в общем, не бессмысленно — как тупой перевод на хаскель программы с Java возможен, но не полезен для нервного здоровья, так и тут было бы вполне логично, если правильный способ писать программу на Idris отличается от такового на Haskell.
Легкая часть (деление слов на фрагменты) у него заняла больше 30 строк, и я не могу сказать, что из аннотаций типов мне очевидно, что она обладает заявленными свойствами. Т.е. она вроде проходит тайп-чекер (сам я не проверял), но мне совершенно не очевиден тот факт, что тот тип, которому соответствует код, выражает именно то свойство, которое должен по замыслу автора. Тяжелую часть он обещал дочистить и выложить на гитхаб. Обещал в июле 2013 г. Я туда сходил. Там до сих пор placeholder. Не осилил, похоже.
И это человек с бэкграундом в виде написания пруфчекера.
Отсель мораль. Затраты на получение бОльшей уверенности, чем предоставляет хаскель — астрономические. Если вы пишете софт, который будет работать автономно в дальнем конце Солнечной системы лет через 20 после запуска, то они могут окупиться. Тогда собирайте команду ОЧЕНЬ хороших программистов с ОЧЕНЬ хорошим математическим бэкграундом, берите заказ у NASA лет на 10 работы (не одного человека а всей команды), пишите очевидный код, и упирайтесь его доказывать. Не пытайтесь писать код, который будет легче скормить пруфчекеру, но который будет не очевиден — это тупиковый путь.
Может быть, дальше средства доказуемого программирования разовьются и будет лучше. Но пока, если вы хотите уверенности в надежности своей программы за вменяемое время, оптимум называется Haskell.