выдавливание инженерного подхода из ИТ приносит хорошие деньги
Это весьма спорное утверждение, хорошие деньги в краткосрочной перспективе приносит найм дешёвых низкоквалифицированных разработчиков, да и то не во всех областях. А вот в долгосрочной перспективе это дорогой и зачастую смертельный для бизнеса подход.
Крупные игроки это уже поняли и сейчас опять восстанавливают серьёзный подход к разработке, но уже на другом уровне, стараются по-прежнему экономить на массовом разработчике, но при этом активно развивают инструменты в рамках групп высококвалифицированных разаработчиков, которые (инструменты) бы позволили снизить требования квалификации к большинству разработчиков (reason, Go, typescript, множество тулов стат. анализа кода и тд.)
Ну и активно используют инженерные методы разработки для наиболее чувствительных частей системы (в конце статьи много ссылок на это).
То есть, определённое понимание есть у некоторых крупных игроков на ранке ПО по поводу того, что нужно иногда софт разрабатывать с серьёзным подходом.
Мотивация думать, развиваться, создавать и творить сведена, можно сказать, к нулю.
Ну тут тоже не всё так однозначно плохо. Например, многие менеджеры (даже топы из весьма крупных компаний) активно изучали/изучают опыт Semco (могу рекомендовать книги Рекардо Семлера "Маверик" и "Выходные всю неделю").
Надеюсь его опыт будет потихоньку перениматься в корпорациях, так как он показал на практике, насколько можно эффективно мотивировать людей, на развитие и работу.
Потом получается: ты его просишь пересмотреть модель в его же коде с учетом изменения бизнеса, а он не помнит что и для чего вообще делал, не то что что-то предложить, т.к. смещены приоритеты и ценности и ему это неинтересно. А ты его уволить не можешь, т.к. менеджменту он выгоден, как дешевый ресурс.
Ну тут проблема менеджмента. Обычно проекты, где менеджеры допускают такой подход к разработке (а особенно, если в результате код на выходе получается не поддерживаемый и не сопровождаемых, то есть с плохим bus-factor), долго не живут.
Чисто интуитивно кажется, что доказывать корректность Rust кода должно быть проще чем сишного.
Как показывает Ron Pressler, фундаментальной разницы в общем случае нет.
У него основная идея — это для определённых классов задач (только нужно сначала ввести продуманную таксономию) разработать DSL'и и спец-средства для проверки кода на этих DSL. За счёт специализации по областям применения и разумного ограничения на DSL'и, можно класс формально верифицированного ПО значительно увеличить.
Но, я предполагаю, что делая свободные верифицированные компоненты вроде того же seL4 мы в какой-то момент можем оказаться в мире где есть верифицированная операционная система пригодная для всего (может кроме домашнего использования).
Хотелось бы в это верить, но тот же самый seL4 накладывает весьма серьёзные ограничения на межмодульное взаимодействие.
Кроме того, в общем случае (общий знаменатель) мы можем рассчитывать на массовый верифицированный софт, который верифицирован только на базовые свойства (типа нет сегфолтов, и пр), а верификация продуктовой-логики всё-равно будет специализирована по конкретным областям применения софта.
Даже к одному и тому же софту в разных областях могут предъявляться существенно разные требования.
Что, на мой взгляд, серьёзно затрудняет появление массового верифицированного софта.
сформулировать корректные требования значительно проще чем корректно реализовать их
В целом кажется так, но думаю иногда может быть и наоборот.
Но в целом задача формулирования требований весьма нетривиальная — нужно понять какие инварианты и предикаты в системе позволяют ей достигать нужных нам характеристик, а это весьма творческий процесс.
Важный момент это возможность прогресса — допустим мы сделали формально верифицированную софтину, а потом, со временем нашли баг в требованиях, исправили их, исправили софтину и снова верифицировали их, в отличии от обычной разработки мы в значительно большей степени уверены, что улучшили наше решение т.к. знаем что правки не внесли багов.
Именно такой подход мне импонирует больше всего, ибо позволяет сдержать экспоненциальный рост костылей в софте по мере изменения функционала и починке багов.
Что самое интересное, что Рон Пресслер(в той статье по ссылке в комментарии) хорошо показывает, что языки на сложность задачи верификации свойств программ влияют слабо, ибо там сложность растёт от самих свойств. И декомпозиция программ не помогает в уменьшении сложности верификации, так как сумма верифицированных частей не равна автоматом верифицированному целому, это целое нужно отдельно верифицировать и сложность явно больше простой суммы сложностей верификации отдельных частей.
То есть задача верификации в общем случает от языков слабо зависит. Если язык тьюринг полный. Можно, конечно, урезать полноту языков, но тогда мы будем сильно сужать область решаемых задач в рамках этих языков.
Что касается более массового, то тут есть пара моментов:
Мне пока не понятно точно, кто в какой области работает из тех, что обратили внимание на статью. То есть, нет понимания того, что было бы интересно большинству
Чтобы грамотно написать пример близкий к реальности из какой-либо области, нужно до какой-то степени знать эту область и понимать её специфику.
В общем я пока в размышлениях относительно того, чтобы такого написать более массового и близкого к реальности.
Есть идея следующую статью посвятить решению одной небольшой реальной задачи из области бизнес-логики и баз данных с использованием TLA+.
Там была проблема, которая тестами практически не ловится, но было интуитивное понимание того, что определённый код может работать некорректно.
Сделали модель и на модели явно нашли ошибку в алгоритме работы.
Теперь нужно убедиться, что модель отражает код (направленный тест по трассе ошибки из модели) и если так, то думать, как исправить алгоритм или как сделать аккуратные костыли (работу которых тоже нужно будет проверить на модели).
Там получается как раз: и модель небольшая, самое оно для учебной, и задача реальная.
Ага, взаимно :) Тоже узнал много новых интересных слов :)
По поводу Coq и определения семантики, вспомнил про статью, которая мне очень понравилась, когда я ещё был RTL-инженером: https://arxiv.org/pdf/1301.4779v1.pdf
Она, конечно про верифицированный синтез железа из спец DSL, но подходы с софтовой верификацией очень близки.
Rest сервис это не про фронт вообще) Во всем, что я описал, 146% бэкенда.
Да, у меня всё ещё немного смещено восприятие, так как бэкенд-разработчик я относительно недавно. После системного программирования, рест тоже больше ассоциируется с фронтом. :)
В общем, пока ещё я не силён в современной фронтэнд и бэкенд веб и мобильной разработке и могу в терминологии и классификациях технологий и фреймфорков что-то и путать (например, про Spring Boot в первый раз прочитал). :(
Боевой пример: схема + условный GraphQL на входе и строго-типизированный результат на выходе. Баги в этой штуке наиболее опасные и приводят к тому, что компилятор превращается в бредогенератор. Код на выходе практически всегда компилится (мы ж все вывели автоматом!) и проходит все статические проверки (у нас ведь отличный транслятор в Java!), полностью документирован (генератор документации тоже не подкачал!), но делает какую-то фигню (упс...).
Про GraphQL не слышал, интересная вещь, посмотрю. Спасибо за наводку.
А что касается синтаксически правильных и правильно типизированных программ, которые делают какую-то фигню — тут уже начинается область семантики и проверки семантической корректности.
Весьма интересная область сама по себе.
Частично семантику можно переложить на типы (особенно сложные системы типов, GADT + эмуляция поведенческих типов, как уже упоминал, или пойти в хардкор: зависимые типы (но это уже весьма сложные дебри чего-то типа Coq, Agda, Idris и пр.))
Как идея: трансляция DSL в Coq, семантика определена заранее в либах Coq (ну не знаю, там например ввиде операционной семантики с малым шагом (автоматические тактики тогда хорошо работают) для предметной области), далее проверка выхлопа кодогенератора DSL->Coq в Coq'е полуавтоматическими тактиками, кодогенерация из Coq в целевой язык (сейчас, по-моему, поддерживает Haskell, Ocaml, scheme).
Но это весьма трудозатратный способ, и полностью автоматическую проверку семантической корректности сделать не получится в общем случае, там может требоваться и ручная работа. Хотя, если семантика простая и написать хорошие тактики, то можно практически всегда автоматически проверять.
Но это так, просто мысли вслух.
Что касается зависимых типов и ATP типа Coq и пр, то у меня весьма скромный опыт работы с ними, так что тут вряд ли чем-то серьёзно смогу помочь.
Ещё как идея: это попробовать использовать SAT/SMT солверы. DSL + контракты -> в формат для SMT и запуск SMT для поиска нарушений контрактов (контрпримеров). Подход а-ля Frama-C + why3 + WP plugin, или ADA/Spark + GNATProve.
В общем, когда начинаются задачи на проверку нетривиальной семантики, начинается самое интересное :)
Нужна новая статья, с подробным разбором создания вебсервиса, например тот же заказ пицы с оплатой, с применением подходов из статьи.
Да, это было бы хорошо.
Только я в основном бэкенд-разработчик, а до этого был системным программистом (а-ля уровня гипервизоров), а ещё раньше вообще логику для микрух и FPGA разрабатывал, поэтому чтобы мне сделать хороший пример со связкой ещё рабочего фронтэнд кода придётся потратить весьма приличное время просто на погружение во фронтэнд разработку.
Именно поэтому я и упомянул в статье блог Hillel Wayne и в частности его статью о применении Alloy при разработке UI. Чтобы люди, которым ближе фронтэнд смогли посмотреть пример и для фронтэнда.
Т.е. в конце должен быть видимый эффект какой-то от возни с Alloy.
Тема графов для микросервисов, начало которой приведено в данной статье, получила продолжение в реальности (как личный проект) и у меня сейчас есть уже наброски работающего прототипа. Возможно, в дальнейшем я и опубликую что-нибудь из продолжения работы относительно графов.
А пока, к сожалению, большинство просто не понимает о чем речь и зачем все эти приседания на непонятном языке.
Тут всё зависит от того, кому какая тематика ближе.
Для кого-то пример на основе фронтэндных задач будет тёмным лесом.
Но в целом да, фронтендеров больше (ну мне так кажется) и лучше было бы понятный пример из этой области.
Но, увы, от области фронтэнда я далёк. Могу только рекомендовать посмотреть блог Hillel Wayne.
Если будет достаточное множество желающих, возможно даже что-то из его блога я и переведу, дополнительно ещё разъяснив непонятные и тонкие моменты.
(если есть интерес к определённым темам, можно мне личку писать, я потом обобщу и в новых статьях постараюсь учесть интересы большинства)
У них ведь ресты, интерфейсы, сервисы, дао, паттерны, а не вот эти вот ваши «вычислительные графы».
А у меня на работе "вычислительные графы" и микросервисы :) Зависит от того, где
кто работает.
Надеюсь я понятно донес свой посыл)
В целом да. Во многом согласен с посылом.
Только, как мне кажется, у фронтендеров запрос на формальные методы и корректное ПО существенно меньше, чем у людей middle и back-end. Чисто ввиду того, что ошибки в бэкенде, на мой взгляд, дороже и сложнее в отладке (плюсовый многопоточный асинхронный код отлаживать намного менее приятно, чем JS для браузера).
Там ясно написано — всё сложно и методов много. Собственно об этом я с самого начала и говорил, но вы упирались, а потом (в предпоследнем ответе) всё же согласились.
По поводу высокой сложности, я имел ввиду ATP, к которым вы почему-то стараетесь всё свести. А model-checkers/model-finders это как раз относительно легко и при небольшой сноровке можно широко применять.
Собственно по статье (по пользе от неё). Вы там пишете про конкретику, по совершенно ненужный синтаксис и тому подобные детали, но не описываете сущность применяемого подхода.
Это да, изначально статья планировалась существенно больше, но тогда охват аудитории был бы ниже. Я же в самом начале написал, что эта статья для привлечения внимания, причём, чтобы большинству разработчиков было интересно, в статье максимум конкретики и примеров, чтобы можно было самим поиграться.
Если бы я начал расписывать SAT/SMT солверы + Kodkod + детальное изложение реляционной логики первого порядка с операторами транзитивного замыкания и join + особенности трансляции всего этого в код задач для SAT/SMT солверов + особенности работы kodkod — кто бы это всё стал читать? 1-2 человека?
И от расписывания внутренностей специально в этой статье старался держаться подальше, ибо хотел показать разработчикам как выглядит именно пример применения Alloy, а не расписать, что у него внутри, как к нему писать плагины, как вызывать kodkod и какие особенности трансляции атомов из kodkod в формулы для SAT солверов.
он довольно внятно и коротко объясняет — я делал сайтик, потом взглянул на него с точки зрения конечных автоматов, потом построил модель автомата и проверил возможные переходы состояний, после чего получил результат, позволивший существенно улучшить сайтик (некоторые страницы были очень далеко, что-то ещё там было нелогично)
Во-первых, я специально дал ссылку для тех, кто захочет подробнее посмотреть на примеры близкие к реальности применения формальных методов.
Во-вторых, он хоть и взял модельный пример из реальной работы, но для статьи его очень сильно упростил.
В-третьих, в статье он делает сильный акцент на какой-то сторонний ресурс для моделирования формочек, а именно про применение самого Alloy у него в той статье очень мало.
Я же решил акцент сместить на применение самого инструмента, именно для того, чтобы лучше показать как с ним работать.
Вместо пояснений о природе инструментов, вы просто даёте название и далее, примерно как в мифах про богов, рассказываете про какие-то магические свойства персонажей. При этом — как это всё работает, вы не поясняете. Ну и зачем мне такая статья?
Цель статьи я обозначил прямо в самом начале: привлечь внимание разработчиков к инструментам определённого толка, которые могли бы им помочь в их работе.
Для тех, кто захочет изучить предмет статьи подробнее, дано много ссылок на разные материалы по теме.
Кроме того, планируются ещё статьи, возможно с более глубоким погружением в детали технологий.
То есть с принципами вы не спорите, с ними согласны, но тогда зачем мне всё остальное?
С какими принципами? Чтобы с чем-то спорить или соглашаться это должно стать предметом дискуссии и быть чётко выраженным.
На текущий момент я вижу непонятную критику того, что я якобы не объяснил, как всё работает, хотя цель статьи была заявлена в самом начале и там ничего про объяснение принципов работы не было.
Мне не синтаксис нужен, мне нужна целостная картина применения инструмента, с упором на сокращение затрат на том или ином этапе разработки. И вот этого у вас просто нет (ну кроме заявлений про «инженерный подход творит чудеса»).
Я бы и сам не против написать детальную статью со всеми ньюансами (в том числе и подкапотными технологиями в основе инструментов) и детальным примером применения с отсылками к промышленному опыту. Но сколько людей смогут прочитать такую статью и осилить? Огромное количество людей изобилие в подобной статье внутренних деталей того же самого Alloy просто отпугнёт. И вместо того, чтобы показать пользу, лёгкость применения и удобство формальных инструментов, я просто всех распугаю и поддержу миф, что нормальная разработка ПО и систем это суперсложно, супердорого и пр.
PS: Ещё раз отдельно для вас: детали внутренностей Alloy можете посмотреть тут, тут, тут, тут ну и по инету много других публикаций.
во-первых IDE ничего не знает про ваши изощрения с деревьями.
Это да, при нетривиальном внешнем DSL все прелести IDE теряются :(
Ну, либо как вариант, сразу делать плагин к IDE хотя бы для подсветки синтаксиса (правда тут сразу возникает тесная привязка к конкретным IDE).
стоимость разработки новой фичи сильно растет, потому что надо заниматься разбором и трансформацией этих самых AST. Ну и верификацией всего этого кода, что тоже стоит дорого. Доказывать-то приходится трансформацию всего поля AST. А в Scala 2 деревья ого-го, и ко всему прочему с атрибутами и мутируемые. Короче вообще адъ и Израиль.
Со Scala я мало знаком (практически не знаком), но в Ocaml с этим не так страшно. Есть инструменты и либы, которые существенно облегчают задачу написания AST трансформеров. Ну и плюс к этому тайп-чекинг всё-равно потом делается, и совсем уж ерунду компилятор не пропустит. Если часть семантики закрыть на GADT + эмуляция поведенческих типов (это будет от пользователя спрятано и появится лишь в результирующем AST), то можно до какой-то степени быть уверенным и в семантической корректности кодогенерации.
Мы так затащили подмножество SQL-92 внутрь нашего языка для поддержки маппинга таблиц и ETL ;-).
Хорошо, когда синтаксис DSL вкладывается в синтаксис целевого языка :)
Одним из самых крутых языков (на мой взгляд) в этом смысле был CommonLisp с его reader macro, когда файл начинается как CommonLisp, а заканчивается как Pascal, после нескольких reader macro :)
В вашей статье, по приведённой ссылке, основной упор делается на верификацию программ и верифицированное ПО (тот же пример с seL4). Ну и плюс упоминаются языки с алгебраическими системами типов и спец-железо под эти языки и тд.
Это хорошо, что такие мысли возникают (надеюсь, у всё большего количества разработчиков), но тут нужно хорошо себе представлять область применения разных технологий, методов и инструментов. И что формальные методы включая формальную верификацию программ — это только одно из условий корректного ПО (необходимое, но не достаточное)
Например:
Невозможно создать очень выразительный язык, чтобы свойства программ на нём легко доказывались. Тут антагонизм — либо ограничиваем выразительность языка, чтобы класс верифицируемых программ был шире, либо жертвуем верифицированностью в угоду большей выразительности. Хорошая статья на эту тему (и смежные темы) у Ron Pressler: Why Writing Correct Software Is Hard
Очень рекомендую всего Рона Преслера, там все материалы отличные.
Задача формулирования свойств для проверки/верификации сама по себе довольно сложная и интересная. И тут, к сожалению, не так уж и много автоматизируется. Всё гипотезы для проверки, контракты, все LTL формулы и пр. должен формулировать разработчик (автоматически там не так много можно сформулировать и почти всё оно будет тривиальным), основываясь на требованиях к ПО.
И тут мы переходим к след. пункту:
Постановка задач и разработка требований — тоже сама по себе довольно сложная задача и мало-автоматизируемая.
Программы (на любых языках, хоть C, хоть Haskell) — это всего-лишь зафиксированные в тексте алгоритмы поведения системы (частей системы, при декомпозиции). И вопрос разработки корректных (для решения какой-либо прикладной задачи) алгоритмов — это тоже нетривиальная и слабоавтоматизируемая задача.
Много базовых алгоритмов (сортировки, поиска и пр) уже разработано, какая-то часть даже формально верифицирована на соответствующие свойства (то что алгоритм qsort действительно сортирует и пр.), но любой практический софт, базируясь на этих "кирпичиках" реализует свой нетривиальный алгоритм, корректность которого — это ещё вопрос.
И много-много других моментов, которые влияют на корректность ПО по отношению к решаемым этим ПО задачам.
Пока что мне не удалось вызвать интерес к этому ни у одного из коллег (объяснял, кидал ссылки на статьи). Типичный ответ — напишем примерные требования максимум, тесты напишем, разве мало?
Да, к сожалению разработчики и менеджеры не понимают, что грамотное применение формальных методов может серьёзно помочь с точки зрения уменьшения затрат на разработку, отладку и поддержку (уменьшением вероятности серьёзных архитектурных багов). Ну и вероятность сдать проект в срок тоже может быть увеличена.
Поэтому и задумал я написать цикл статей, где бы в простой форме можно было показать как применять тот или иной метод и инструмент.
Лично я понял полезность TLA+, когда занимался отладкой рандеву для многопоточного кода. Отлаживать нетривиальную синхронизацию в многопоточке — это сущий ад. На TLA+ нашёл ошибку в алгоритме (он хоть и базировался на Лэмпортовском, но был динамическим по количеству участников рандеву), ну и соответственно правил реализацию. Ошибка была на 63 шаге модели при поиске в ширину. То есть на тестах найти и отладить такое — нереально.
А в целом примерно так: Alloy для моделирования структур, топологий и конфигураций и небольшой операционной семантики над ними (то есть, когда структура бедна форматами данных, функциями и пр., но богата связями/отношениями между объектами с большим количеством логики поверх этих отношений), а TLA+ когда много динамики с богатыми структурами данных (множества, записи, функции и пр).
Грубо говоря: статика (топология, конфигурации) — это Alloy, а динамика (протоколы, FSM и тд) — это TLA+. Хотя до какой-то степени они взаимозаменяемы. Например, я нормально моделировал FSM и в Alloy.
А где будет храниться спецификация? Прямо в проекте или отдельно?
Если рассматриваем спеку в формальном смысле (текст на TLA+/Alloy), то тут зависит от уровня абстракции: абстрактные спеки ближе к диз-докам и высокоуровневой докуменатации проекта, детальные спеки уже ближе к коду (либо даже в код в комментарии и настроить систему CI, чтобы она в одном из шагов вырезала спеки из исходников и прогоняла их проверку в тулах моделирования).
Ещё есть небольшой плюс: Alloy позволяет получать диаграммы конфигураций системы в виде картинок, что позволяет их потом использовать в доках, и для TLA+ тоже есть модуль анимации трасс: https://github.com/will62794/tlaplus_animation. Это позволяет при небольшой сноровке из моделей получать сопровождающие картинки для документации. Например, в текущей статье все диаграммы взяты из Alloy (с небольшими правками).
Спецификацию пишут на функцию, класс или в отдельных случаях лишь на модуль (если функции и классы малы и понятны)?
Тут всё зависит от потребности. Где-то достаточно высокоуровневых спек, на абстрактном архитектурном уровне, где-то нужны более детальные.
Хорошо процесс применения спек описан в OpenCom RTOS
В общем где, как и на каком уровне детализации применять спеки зависит от конкретного проекта и конкретных потребностей. Понимание этого приходит по мере изучения методов и примеров их применения в промышленности.
Часто можно спеки применять ретроспективно, например, чтобы промоделировать подозрительные части системы, в корректности которых есть сомнения (в распределённых системах на тестах далеко не всё можно найти).
Было бы здорово, если бы вы помогли сделать первые шаги, как это делают современные курсы по обучению. Это вызовет интерес и далее человеку будет гораздо проще двигаться.
Тут не совсем понял. На какие-либо курсы у меня точно не хватит ни сил, ни времени.
Пока постараюсь только цикл статей обзорных с небольшими примерами сделать.
Советую посмотреть блог Hillel Wayne (уже многократно тут на него ссылался), у него много простых примеров применения формальных спек и моделирования.
Относительно TLA+ могу рекомендовать его же книгу Practical TLA+. Относительно простое введение в использование TLA+ с простыми примерами. Для начала — самое оно.
У меня есть данные по проекту, было бы интересно посмотреть, как можно было бы ускорить разработку, если применять инженерный подход.
С этим, наверное, лучше в личку. Может, после обсуждения получится на интересную статью материал сделать (при согласовании того, какие детали допустимо выносить на публикацию).
Ну вот, а вы давеча говорили, что инструмент, мол, стал доступнее…
Вы специально троллите? Или просто настолько невнимательно читаете?
Писал в статье я про класс инструментов, которые весьма существенно отличаются от ATP. Приравнивать Isabelle/HOL к Alloy — это показывает полную неосведомлённость в вопросе.
И в первую очередь про инструменты классов model-checkers/model-finders я говорил, что они стали намного удобнее и доступнее.
А вы на автоматах с помощью указанных в статье инструментов это сможете? В смысле асинхронный обмен в них вообще поддерживается?
Сравните сложность. Думаю разница явно видна. И доказательство в Isabelle/HOL появилось спустя много лет TLA+ модели. И, что самое забавное, базируется именно на TLA+ модели.
И да, даже если некое частное решение всё же можно сделать на ваших инструментах, то всё равно это бесконечно малая часть от реальной потребности. Ну хоть с этим-то вы согласны?
С чем согласен? С вашими утверждениями, которые непонятно на чём основаны с учётом того, что вы вообще не вникаете в ответы на ваши комментарии и не читали статью (есть веские основания это полагать)?
Гуглите isabelle theorem prover. От него по встретившимся терминам найдёте массу аналогов.
Рад, что вы знакомы с ATP. Но это только небольшая часть инструментария для инженерного подхода.
И применение ATP:
Очень дорогое, требующее высокой квалификации
Подходит только для весьма узких задач (докажите мне пожалуйста корректность алгоритма Paxos с помощью Isabelle/HOL)
Требует частого ручного вмешательства пользователя в ходе доказательства свойств ПО (ну да, после этого кодогенерация автоматом, хотя и то, только для определённого подмножества целевого языка и как правило ещё и с хаками системы типов этого целевого языка (здравствуй obj.magic в Ocaml и аналоги в Хаскеле), либо генерация в бестиповый ЯП, типа scheme)
Здорово, что кто-то переводит статьи Hillel Wayne. Жаль, что мало.
Спасибо за ссылку!
Это весьма спорное утверждение, хорошие деньги в краткосрочной перспективе приносит найм дешёвых низкоквалифицированных разработчиков, да и то не во всех областях. А вот в долгосрочной перспективе это дорогой и зачастую смертельный для бизнеса подход.
Крупные игроки это уже поняли и сейчас опять восстанавливают серьёзный подход к разработке, но уже на другом уровне, стараются по-прежнему экономить на массовом разработчике, но при этом активно развивают инструменты в рамках групп высококвалифицированных разаработчиков, которые (инструменты) бы позволили снизить требования квалификации к большинству разработчиков (reason, Go, typescript, множество тулов стат. анализа кода и тд.)
Ну и активно используют инженерные методы разработки для наиболее чувствительных частей системы (в конце статьи много ссылок на это).
То есть, определённое понимание есть у некоторых крупных игроков на ранке ПО по поводу того, что нужно иногда софт разрабатывать с серьёзным подходом.
Ну тут тоже не всё так однозначно плохо. Например, многие менеджеры (даже топы из весьма крупных компаний) активно изучали/изучают опыт Semco (могу рекомендовать книги Рекардо Семлера "Маверик" и "Выходные всю неделю").
Надеюсь его опыт будет потихоньку перениматься в корпорациях, так как он показал на практике, насколько можно эффективно мотивировать людей, на развитие и работу.
Ну тут проблема менеджмента. Обычно проекты, где менеджеры допускают такой подход к разработке (а особенно, если в результате код на выходе получается не поддерживаемый и не сопровождаемых, то есть с плохим bus-factor), долго не живут.
red — интересный проект, по мотивам REBOL, который когда-то мне показался весьма оригинальным, и сейчас меня даже удивило, что он ещё жив :)
Как показывает Ron Pressler, фундаментальной разницы в общем случае нет.
У него основная идея — это для определённых классов задач (только нужно сначала ввести продуманную таксономию) разработать DSL'и и спец-средства для проверки кода на этих DSL. За счёт специализации по областям применения и разумного ограничения на DSL'и, можно класс формально верифицированного ПО значительно увеличить.
А что в основе планируется? DHT? Kedemlia?
Хотелось бы в это верить, но тот же самый seL4 накладывает весьма серьёзные ограничения на межмодульное взаимодействие.
Кроме того, в общем случае (общий знаменатель) мы можем рассчитывать на массовый верифицированный софт, который верифицирован только на базовые свойства (типа нет сегфолтов, и пр), а верификация продуктовой-логики всё-равно будет специализирована по конкретным областям применения софта.
Даже к одному и тому же софту в разных областях могут предъявляться существенно разные требования.
Что, на мой взгляд, серьёзно затрудняет появление массового верифицированного софта.
В целом кажется так, но думаю иногда может быть и наоборот.
Но в целом задача формулирования требований весьма нетривиальная — нужно понять какие инварианты и предикаты в системе позволяют ей достигать нужных нам характеристик, а это весьма творческий процесс.
Именно такой подход мне импонирует больше всего, ибо позволяет сдержать экспоненциальный рост костылей в софте по мере изменения функционала и починке багов.
Что самое интересное, что Рон Пресслер(в той статье по ссылке в комментарии) хорошо показывает, что языки на сложность задачи верификации свойств программ влияют слабо, ибо там сложность растёт от самих свойств. И декомпозиция программ не помогает в уменьшении сложности верификации, так как сумма верифицированных частей не равна автоматом верифицированному целому, это целое нужно отдельно верифицировать и сложность явно больше простой суммы сложностей верификации отдельных частей.
То есть задача верификации в общем случает от языков слабо зависит. Если язык тьюринг полный. Можно, конечно, урезать полноту языков, но тогда мы будем сильно сужать область решаемых задач в рамках этих языков.
enaml — интересная вещь, спасибо за ссылку!
Что касается более массового, то тут есть пара моментов:
Мне пока не понятно точно, кто в какой области работает из тех, что обратили внимание на статью. То есть, нет понимания того, что было бы интересно большинству
Чтобы грамотно написать пример близкий к реальности из какой-либо области, нужно до какой-то степени знать эту область и понимать её специфику.
В общем я пока в размышлениях относительно того, чтобы такого написать более массового и близкого к реальности.
Есть идея следующую статью посвятить решению одной небольшой реальной задачи из области бизнес-логики и баз данных с использованием TLA+.
Там была проблема, которая тестами практически не ловится, но было интуитивное понимание того, что определённый код может работать некорректно.
Сделали модель и на модели явно нашли ошибку в алгоритме работы.
Теперь нужно убедиться, что модель отражает код (направленный тест по трассе ошибки из модели) и если так, то думать, как исправить алгоритм или как сделать аккуратные костыли (работу которых тоже нужно будет проверить на модели).
Там получается как раз: и модель небольшая, самое оно для учебной, и задача реальная.
Ага, взаимно :) Тоже узнал много новых интересных слов :)
По поводу Coq и определения семантики, вспомнил про статью, которая мне очень понравилась, когда я ещё был RTL-инженером: https://arxiv.org/pdf/1301.4779v1.pdf
Она, конечно про верифицированный синтез железа из спец DSL, но подходы с софтовой верификацией очень близки.
Если есть интерес к хардкорной верификации, то могу рекомендовать: https://softwarefoundations.cis.upenn.edu/index.html
Там как раз про семантику софта и верификацию много информации.
Да, у меня всё ещё немного смещено восприятие, так как бэкенд-разработчик я относительно недавно. После системного программирования, рест тоже больше ассоциируется с фронтом. :)
Бэкенд больше ассоциируется с какой-нибудь плюсовой многопоточкой, что-то похожее на вот такие вещи: https://github.com/vasil-sd/rendezvous-protocol
В общем, пока ещё я не силён в современной фронтэнд и бэкенд веб и мобильной разработке и могу в терминологии и классификациях технологий и фреймфорков что-то и путать (например, про Spring Boot в первый раз прочитал). :(
Про GraphQL не слышал, интересная вещь, посмотрю. Спасибо за наводку.
А что касается синтаксически правильных и правильно типизированных программ, которые делают какую-то фигню — тут уже начинается область семантики и проверки семантической корректности.
Весьма интересная область сама по себе.
Частично семантику можно переложить на типы (особенно сложные системы типов, GADT + эмуляция поведенческих типов, как уже упоминал, или пойти в хардкор: зависимые типы (но это уже весьма сложные дебри чего-то типа Coq, Agda, Idris и пр.))
Как идея: трансляция DSL в Coq, семантика определена заранее в либах Coq (ну не знаю, там например ввиде операционной семантики с малым шагом (автоматические тактики тогда хорошо работают) для предметной области), далее проверка выхлопа кодогенератора DSL->Coq в Coq'е полуавтоматическими тактиками, кодогенерация из Coq в целевой язык (сейчас, по-моему, поддерживает Haskell, Ocaml, scheme).
Но это весьма трудозатратный способ, и полностью автоматическую проверку семантической корректности сделать не получится в общем случае, там может требоваться и ручная работа. Хотя, если семантика простая и написать хорошие тактики, то можно практически всегда автоматически проверять.
Но это так, просто мысли вслух.
Что касается зависимых типов и ATP типа Coq и пр, то у меня весьма скромный опыт работы с ними, так что тут вряд ли чем-то серьёзно смогу помочь.
Ещё как идея: это попробовать использовать SAT/SMT солверы. DSL + контракты -> в формат для SMT и запуск SMT для поиска нарушений контрактов (контрпримеров). Подход а-ля Frama-C + why3 + WP plugin, или ADA/Spark + GNATProve.
В общем, когда начинаются задачи на проверку нетривиальной семантики, начинается самое интересное :)
Рад, что вам понравилась эта книга!
Это реально хорошая книга для первого знакомства с TLA+. Её смело можно рекомендовать всем разработчикам.
Думаю многим дальше PlusCal и не потребуется погружаться в ньюансы TLA+.
Но если вдруг нужно будет чуть больше low-level деталей могу рекомендовать виде-курс самого Лэмпорта: http://lamport.azurewebsites.net/video/videos.html
Затем его книгу "Specifying Systems": https://lamport.azurewebsites.net/tla/book-02-08-08.pdf
И ещё у Рона Преслера можно почитать цикл статей: https://pron.github.io/posts/tlaplus_part1
Вообще у Рона можно всё читать, он хорошо и доходчиво объясняет многие сложные вещи. Но это если есть сильный интерес к Computer Science.
Ещё у Hillel Wayne и Ron Pressler есть довольно много видео с выступлений на различных конференциях, можно на YouTube поискать.
Да, это было бы хорошо.
Только я в основном бэкенд-разработчик, а до этого был системным программистом (а-ля уровня гипервизоров), а ещё раньше вообще логику для микрух и FPGA разрабатывал, поэтому чтобы мне сделать хороший пример со связкой ещё рабочего фронтэнд кода придётся потратить весьма приличное время просто на погружение во фронтэнд разработку.
Именно поэтому я и упомянул в статье блог Hillel Wayne и в частности его статью о применении Alloy при разработке UI. Чтобы люди, которым ближе фронтэнд смогли посмотреть пример и для фронтэнда.
Тема графов для микросервисов, начало которой приведено в данной статье, получила продолжение в реальности (как личный проект) и у меня сейчас есть уже наброски работающего прототипа. Возможно, в дальнейшем я и опубликую что-нибудь из продолжения работы относительно графов.
Тут всё зависит от того, кому какая тематика ближе.
Для кого-то пример на основе фронтэндных задач будет тёмным лесом.
Но в целом да, фронтендеров больше (ну мне так кажется) и лучше было бы понятный пример из этой области.
Но, увы, от области фронтэнда я далёк. Могу только рекомендовать посмотреть блог Hillel Wayne.
Если будет достаточное множество желающих, возможно даже что-то из его блога я и переведу, дополнительно ещё разъяснив непонятные и тонкие моменты.
(если есть интерес к определённым темам, можно мне личку писать, я потом обобщу и в новых статьях постараюсь учесть интересы большинства)
А у меня на работе "вычислительные графы" и микросервисы :) Зависит от того, где
кто работает.
В целом да. Во многом согласен с посылом.
Только, как мне кажется, у фронтендеров запрос на формальные методы и корректное ПО существенно меньше, чем у людей middle и back-end. Чисто ввиду того, что ошибки в бэкенде, на мой взгляд, дороже и сложнее в отладке (плюсовый многопоточный асинхронный код отлаживать намного менее приятно, чем JS для браузера).
По поводу высокой сложности, я имел ввиду ATP, к которым вы почему-то стараетесь всё свести. А model-checkers/model-finders это как раз относительно легко и при небольшой сноровке можно широко применять.
Это да, изначально статья планировалась существенно больше, но тогда охват аудитории был бы ниже. Я же в самом начале написал, что эта статья для привлечения внимания, причём, чтобы большинству разработчиков было интересно, в статье максимум конкретики и примеров, чтобы можно было самим поиграться.
Если бы я начал расписывать SAT/SMT солверы + Kodkod + детальное изложение реляционной логики первого порядка с операторами транзитивного замыкания и join + особенности трансляции всего этого в код задач для SAT/SMT солверов + особенности работы kodkod — кто бы это всё стал читать? 1-2 человека?
И от расписывания внутренностей специально в этой статье старался держаться подальше, ибо хотел показать разработчикам как выглядит именно пример применения Alloy, а не расписать, что у него внутри, как к нему писать плагины, как вызывать kodkod и какие особенности трансляции атомов из kodkod в формулы для SAT солверов.
Во-первых, я специально дал ссылку для тех, кто захочет подробнее посмотреть на примеры близкие к реальности применения формальных методов.
Во-вторых, он хоть и взял модельный пример из реальной работы, но для статьи его очень сильно упростил.
В-третьих, в статье он делает сильный акцент на какой-то сторонний ресурс для моделирования формочек, а именно про применение самого Alloy у него в той статье очень мало.
Я же решил акцент сместить на применение самого инструмента, именно для того, чтобы лучше показать как с ним работать.
Цель статьи я обозначил прямо в самом начале: привлечь внимание разработчиков к инструментам определённого толка, которые могли бы им помочь в их работе.
Для тех, кто захочет изучить предмет статьи подробнее, дано много ссылок на разные материалы по теме.
Кроме того, планируются ещё статьи, возможно с более глубоким погружением в детали технологий.
С какими принципами? Чтобы с чем-то спорить или соглашаться это должно стать предметом дискуссии и быть чётко выраженным.
На текущий момент я вижу непонятную критику того, что я якобы не объяснил, как всё работает, хотя цель статьи была заявлена в самом начале и там ничего про объяснение принципов работы не было.
Я бы и сам не против написать детальную статью со всеми ньюансами (в том числе и подкапотными технологиями в основе инструментов) и детальным примером применения с отсылками к промышленному опыту. Но сколько людей смогут прочитать такую статью и осилить? Огромное количество людей изобилие в подобной статье внутренних деталей того же самого Alloy просто отпугнёт. И вместо того, чтобы показать пользу, лёгкость применения и удобство формальных инструментов, я просто всех распугаю и поддержу миф, что нормальная разработка ПО и систем это суперсложно, супердорого и пр.
PS: Ещё раз отдельно для вас: детали внутренностей Alloy можете посмотреть тут, тут, тут, тут ну и по инету много других публикаций.
Это да, при нетривиальном внешнем DSL все прелести IDE теряются :(
Ну, либо как вариант, сразу делать плагин к IDE хотя бы для подсветки синтаксиса (правда тут сразу возникает тесная привязка к конкретным IDE).
Со Scala я мало знаком (практически не знаком), но в Ocaml с этим не так страшно. Есть инструменты и либы, которые существенно облегчают задачу написания AST трансформеров. Ну и плюс к этому тайп-чекинг всё-равно потом делается, и совсем уж ерунду компилятор не пропустит. Если часть семантики закрыть на GADT + эмуляция поведенческих типов (это будет от пользователя спрятано и появится лишь в результирующем AST), то можно до какой-то степени быть уверенным и в семантической корректности кодогенерации.
Хорошо, когда синтаксис DSL вкладывается в синтаксис целевого языка :)
Одним из самых крутых языков (на мой взгляд) в этом смысле был CommonLisp с его reader macro, когда файл начинается как CommonLisp, а заканчивается как Pascal, после нескольких reader macro :)
В вашей статье, по приведённой ссылке, основной упор делается на верификацию программ и верифицированное ПО (тот же пример с seL4). Ну и плюс упоминаются языки с алгебраическими системами типов и спец-железо под эти языки и тд.
Это хорошо, что такие мысли возникают (надеюсь, у всё большего количества разработчиков), но тут нужно хорошо себе представлять область применения разных технологий, методов и инструментов. И что формальные методы включая формальную верификацию программ — это только одно из условий корректного ПО (необходимое, но не достаточное)
Например:
Невозможно создать очень выразительный язык, чтобы свойства программ на нём легко доказывались. Тут антагонизм — либо ограничиваем выразительность языка, чтобы класс верифицируемых программ был шире, либо жертвуем верифицированностью в угоду большей выразительности. Хорошая статья на эту тему (и смежные темы) у Ron Pressler: Why Writing Correct Software Is Hard
Очень рекомендую всего Рона Преслера, там все материалы отличные.
Задача формулирования свойств для проверки/верификации сама по себе довольно сложная и интересная. И тут, к сожалению, не так уж и много автоматизируется. Всё гипотезы для проверки, контракты, все LTL формулы и пр. должен формулировать разработчик (автоматически там не так много можно сформулировать и почти всё оно будет тривиальным), основываясь на требованиях к ПО.
И тут мы переходим к след. пункту:
Постановка задач и разработка требований — тоже сама по себе довольно сложная задача и мало-автоматизируемая.
Программы (на любых языках, хоть C, хоть Haskell) — это всего-лишь зафиксированные в тексте алгоритмы поведения системы (частей системы, при декомпозиции). И вопрос разработки корректных (для решения какой-либо прикладной задачи) алгоритмов — это тоже нетривиальная и слабоавтоматизируемая задача.
Много базовых алгоритмов (сортировки, поиска и пр) уже разработано, какая-то часть даже формально верифицирована на соответствующие свойства (то что алгоритм qsort действительно сортирует и пр.), но любой практический софт, базируясь на этих "кирпичиках" реализует свой нетривиальный алгоритм, корректность которого — это ещё вопрос.
И много-много других моментов, которые влияют на корректность ПО по отношению к решаемым этим ПО задачам.
Немного прокомментирую по пунктам:
Да, к сожалению разработчики и менеджеры не понимают, что грамотное применение формальных методов может серьёзно помочь с точки зрения уменьшения затрат на разработку, отладку и поддержку (уменьшением вероятности серьёзных архитектурных багов). Ну и вероятность сдать проект в срок тоже может быть увеличена.
Поэтому и задумал я написать цикл статей, где бы в простой форме можно было показать как применять тот или иной метод и инструмент.
Лично я понял полезность TLA+, когда занимался отладкой рандеву для многопоточного кода. Отлаживать нетривиальную синхронизацию в многопоточке — это сущий ад. На TLA+ нашёл ошибку в алгоритме (он хоть и базировался на Лэмпортовском, но был динамическим по количеству участников рандеву), ну и соответственно правил реализацию. Ошибка была на 63 шаге модели при поиске в ширину. То есть на тестах найти и отладить такое — нереально.
Тут имеет смысл посмотреть на промышленный опыт применения этих тулов. Например у амазона есть сравнение Alloy vs. TLA+ для их задач: https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf
А в целом примерно так: Alloy для моделирования структур, топологий и конфигураций и небольшой операционной семантики над ними (то есть, когда структура бедна форматами данных, функциями и пр., но богата связями/отношениями между объектами с большим количеством логики поверх этих отношений), а TLA+ когда много динамики с богатыми структурами данных (множества, записи, функции и пр).
Грубо говоря: статика (топология, конфигурации) — это Alloy, а динамика (протоколы, FSM и тд) — это TLA+. Хотя до какой-то степени они взаимозаменяемы. Например, я нормально моделировал FSM и в Alloy.
Если рассматриваем спеку в формальном смысле (текст на TLA+/Alloy), то тут зависит от уровня абстракции: абстрактные спеки ближе к диз-докам и высокоуровневой докуменатации проекта, детальные спеки уже ближе к коду (либо даже в код в комментарии и настроить систему CI, чтобы она в одном из шагов вырезала спеки из исходников и прогоняла их проверку в тулах моделирования).
Ещё есть небольшой плюс: Alloy позволяет получать диаграммы конфигураций системы в виде картинок, что позволяет их потом использовать в доках, и для TLA+ тоже есть модуль анимации трасс: https://github.com/will62794/tlaplus_animation. Это позволяет при небольшой сноровке из моделей получать сопровождающие картинки для документации. Например, в текущей статье все диаграммы взяты из Alloy (с небольшими правками).
Тут всё зависит от потребности. Где-то достаточно высокоуровневых спек, на абстрактном архитектурном уровне, где-то нужны более детальные.
Хорошо процесс применения спек описан в OpenCom RTOS
В общем где, как и на каком уровне детализации применять спеки зависит от конкретного проекта и конкретных потребностей. Понимание этого приходит по мере изучения методов и примеров их применения в промышленности.
Часто можно спеки применять ретроспективно, например, чтобы промоделировать подозрительные части системы, в корректности которых есть сомнения (в распределённых системах на тестах далеко не всё можно найти).
Тут не совсем понял. На какие-либо курсы у меня точно не хватит ни сил, ни времени.
Пока постараюсь только цикл статей обзорных с небольшими примерами сделать.
Советую посмотреть блог Hillel Wayne (уже многократно тут на него ссылался), у него много простых примеров применения формальных спек и моделирования.
Относительно TLA+ могу рекомендовать его же книгу Practical TLA+. Относительно простое введение в использование TLA+ с простыми примерами. Для начала — самое оно.
С этим, наверное, лучше в личку. Может, после обсуждения получится на интересную статью материал сделать (при согласовании того, какие детали допустимо выносить на публикацию).
Вы специально троллите? Или просто настолько невнимательно читаете?
Писал в статье я про класс инструментов, которые весьма существенно отличаются от ATP. Приравнивать Isabelle/HOL к Alloy — это показывает полную неосведомлённость в вопросе.
И в первую очередь про инструменты классов model-checkers/model-finders я говорил, что они стали намного удобнее и доступнее.
Paxos:
TLA+: https://github.com/bringhurst/tlaplus/tree/master/examples/Paxos
Isabelle/HOL: https://www.isa-afp.org/browser_info/current/AFP/DiskPaxos/outline.pdf
Сравните сложность. Думаю разница явно видна. И доказательство в Isabelle/HOL появилось спустя много лет TLA+ модели. И, что самое забавное, базируется именно на TLA+ модели.
С чем согласен? С вашими утверждениями, которые непонятно на чём основаны с учётом того, что вы вообще не вникаете в ответы на ваши комментарии и не читали статью (есть веские основания это полагать)?
Рад, что вы знакомы с ATP. Но это только небольшая часть инструментария для инженерного подхода.
И применение ATP: