Хабр Курсы для бэкендеров
РЕКЛАМА
Практикум, Хекслет, SkyPro, авторские курсы — собрали всех и попросили скидки. Осталось выбрать!
Поток Бэкенд доступен 24/7 благодаря поддержке друзей Хабра
Комментарии 45
За попытку +.
По делу:
1.
Я лично написал ажно целую библиотеку поддержки FSM с «верификацмями» на эликсире, но это, конечно, были костыли, сделанные из палок.
Зачем было делать "костыли из палок", когда 50% статей на Хабре выражает призыв не делать костылей, + плач Ярославны (Иеремии в девичестве) что массовый IT - это сфера костылестроения.
2
В Cure из коробки есть настоящие верифицируемые конечные автоматы:
Хэлоуворд
record TrafficLight do
cycles: Int
emergency_stops: Int
end
fsm TrafficLight{cycles: 0, emergency_stops: 0} do
Red --> |timer| Green
Green --> |timer| Yellow
Yellow --> |timer| Red
Green --> |emergency| Red
Yellow --> |emergency| Red
end
Z3 проверит, что: ① нет зацикливания (deadlock’ов), ② все состояния достижимы, ③ нет недоопределенных переходов, и ④ инварианты сохраняются. И всё это на этапе компиляции
Ставший порочной традицией пример с хэлоувордом на новом языке не убеждает, а вызывает непонимание и недоверие.
FSM - это идея, правда описанная на языке математики, как оформлять объекты, чьё пространство состояний заранее определено (известно).
Вы берёте объект из двух элементарных множеств "cycles" и " emergency_stops" задаёте на нём функцию переходов отношением (ака "таблицей" сопоставлений, говоря по-народному).
Но даже в простых реальных задачах функция переходов задана составными математическими функциями. И хэлоувордные примеры имеют к ним то же отношение, что программа выводящая известную строку к реальной программе на языке программирования.
Пример. Сейчас дабы позабавиться и поучиться оформляем набором конечных автоматов игру. В тетрисном "стакане", вместо фигургок падает квадрат с игрой крестики-нолики. При проигрыше он падает вниз и складывается вниз "как песок", при выигрыше игрок может "вычеркнуть" любую строку квадратиков с дна стакана.
Очевидно, что уже в этом достаточно простом учебном примере пространство состояний объекта гораздо сложнее хэлоувордного. А функция переключения состояния при падении квадрата - отнюдь не похожа на отношение, заданное вручную над двумя элементарными множествами из 2-х и 3-х элементов. (пикантности добавляет и отображение геометрических множеств в алгебраические/элементарные - и обратно).
Вопросы: как Cure справляется с просчётом таких пространств состояний? чем Cure может помочь при алгоритмическом оформлении клсса подобных задач? (фактически все "клеточные" игры: тетрисы, минёры, питоны, бомберы, итп.)
За попытку +.
Спасибо, век такой доброты не забуду.
Зачем было делать «костыли из палок»
Потому что на неверифицируемых языках иначе не получится.
когда 50% статей на Хабре
Я не читаю Хабр, я читаю профессиональные форумы.
не убеждает, а вызывает непонимание и недоверие
Бывает. Я не ставил перед собой цель убедить, и, тем паче, завоевать доверие.
функция переходов задана составными математическими функциями
Конечно. В тексте есть ссылка на сложный пример с обработчиками переходов.
как Cure справляется с просчётом таких пространств состояний?
Никак. Cure делегирует это SMT-солверу (Z3 по умолчанию). Об этом написано в тексте выше. Как справляется Z3? — Да неплохо, вроде.
чем Cure может помочь при алгоритмическом оформлении клсса подобных задач?
Там в тексте есть ссылки на математическое обоснование. Пересказывать курс теорката и диссер Алессандро Джианолы я тут не планировал. Если вкратце — вместо вашего велосипеда из палок, Cure поможет сделать настоящий верифицированный конечный автомат.
А если я напишу программу, которая будет в цикле для всех целых применять шаги последовательности коллаца, то солвер докажет, что это всегда придет к последовательности 1-2-4-1... ?)))
Нет, отвалится по таймауту и сообщит о нетотальности вашей функции. Нетотальные функции априори не годятся в качестве инструмента построения прикладного ПО.
Заметьте, я серьёзно ответил на ваши неудачные потуги сострить.
Это не потуги, а намек на то что проблема останова (то есть достижения любого состояния) является классической алгоритмически неразрешимой проблемой, соответственно весь путь тупиковый - будет работать только на игрушечных примерах
будет работать только на игрушечных примерах
Это облыжный вывод. Хотя бы потому, что тогда в принципе программирование — будет работать только на игрушечных примерах.
Cure пока не умеет выводить тотальность, но научится. На идрисе (как я говорил в тексте) я годами проектировал критические части далеко не игрушечных примеров.
Если ножом можно зарезать человека, это не значит, что ножи нужно изъять из обращения, или что они бесполезны. По такой логике в первую голову бесполезны тесты, потому что не существует гарантий полного покрытия (даже с мутациями и property-based тестированием).
Можете рассказать подробнее какого рода проектирование вы делали на идрисе? И собственно почему там была важна формальная верификация.
Язык (идрис) вообще классный, вот только развивается очень медленно. Искренне надеюсь что ваш проект будет развиваться быстрее.
Да любого; триггернулось что-нибудь для клиета — у него должно особенным образом измениться состояние трех счетов и пятнадцати правил, но так, чтобы всё осталось консистентным.
Прям совсем подробности не могу, наверное, да и не очень нужно, надеюсь, смысл понятен.
Нужно это было потому, что цена вопроса измерялась миллионами.
Да нет, конечно. В системах с конечной памятью (т.е. на всех реальных) проблема останова отсутствует.
Проблема останова отсутствует, проблема тотальности функций (завершения за конечное время) — нет. Я так понял, речь про второе.
Если к системам с конечной памятью относиться не как к реальным реализациям идеализированной бесконечной МТ, то на этих системах даже коммутативность сложения на ℕ не докажешь, потому что непонятно, терм
+-comm : (x y : ℕ) → x + y ≡ y + xтотален «потому», что он логически консистентен и действительно выражает известное утверждение о ℕ, или же потому, что на данной конкретной машине просто тупо перебрали все влезающие в память натуральные числа, и утверждение это, соответственно, не о всех натуральных числах, а о числах меньше данного.
Зачем такое нужно, непонятно.
Правда, зачем называть обёртку над SMT прувером и ставить её в один ряд с завтипами, тоже непонятно, но это уже вопрос ОПу. Среди других вопросов ОПу: @cupraer, типобезопасный printf на вашей версии завтипов пишется? Какой положняк по экстенсиональности и всяким другим умным словам?
Я вроде не называл SMT прувером, я использовал слово «солвер». Завтипы — завтипами, солвер — солвером. Я не стремился поставить их в один ряд, скромно через запятую.
типобезопасный printf на вашей версии завтипов пишется?
Нет. И я не уверен, «пока нет», или «вообще нет». Я практик, и я вынужден признать, что основы математики слишком сильно подзабыл, или просто отупел с годами (хотя был бы очень рад подсказкам, советам и критике). На данном этапе мне проще полностью отказаться от эффектов и IO. Сейчас print существует только ради отладки, в дальнейшем я пока планирую его выкинуть и добавить отсылку сообщения (акторная модель же).
Цель этого языка существенно отличается от академических (я где-то на эрланг-форуме даже написал, что мой девиз — «succeed at any cost»). Я решал свою задачу: кусок кода, подсистема, которая компилируется в BEAM, и которую можно легко и прозрачно слинковать снаружи хоть из эликсира, хоть из глима, хоть из лфе. хоть из эрланга.
У меня даже есть curify функция, которая возьмет код на эрланге и скажет тайп-чекеру: тут чувак знает, что делает, типы вот такие, отстань.
На данном этапе мне проще полностью отказаться от эффектов и IO.
Тут дело не в IO (считайте, что это sprintf, а не printf), а в том, что в полноценных завтипах вы можете написать функцию вроде
PrintfType : String → Type
PrintfType ("%d" :: rest) = Int → PrintfType rest
PrintfType ("%f" :: rest) = Float → PrintfType rest
...
PrintfType "" = Stringи потом
printf : (fmt : String) → PrintfType fmtпосле чего, скажем, у printf "Age: %d, weight: %f" будет тип Int → Float → String
Да какое нафиг ℕ на машинах с конечной памятью, о чём вы? Речь может идти только о кольце остатков по модулю (Zm), а в этом случае всё хорошо доказывается.
Обычное ℕ. На машинах с конечной памятью (и в тетрадках с конечным числом листов) вы вполне себе можете доказывать вещи про бесконечный ℕ.
И это на самом деле полезно, потому что как-то очень глупо перепроверять все доказательства и ждать 2^100500 времени после того, как вы просто купили железку с памятью чутка побольше.
Теоретически - да. Практически - разницы нет, пара вложенных циклов по bigint уже превышает время жизни вселенной на порядки
Так задача вроде не выполнить цикл, а доказать, что он не выполнится.
Просто как бы куча различных линтеров и компиляторов именно этим и занимаются, в т.ч. умеют детектировать бесконечные циклы
читаю профессиональные форумы
Это, например, какие?
https://erlangforums.com/, https://elixirforum.com/, https://devtalk.com/, и типа того.
Для не-хеллоуворлдов есть HSM/statecharts
Наконец-то нормальная статья от вас. В адекватном тоне и без замашек на бога программирования. Завтипы это будущее, неистово одобряю.
В адекватном тоне и без замашек на бога программирования.
Значит, текст ужасен. Надо переписывать.
Завтипы это будущее, неистово одобряю.
Если серьезно, то я не согласен. К великому сожалению.
Критической массы заинтересованных в том, чтобы делать не тяп-ляп, а верифицировать — не честным словом и не одним крылом, — исчезающе мало. Бизнесу это не выгодно, потому что долго. Проще и выгоднее прилечь на полдня, или отправить пару доверчивых владельцев автопилотов сотого поколения — в столб на полной скорости.
Еще это всё слишком сложно. У меня высшее математическое образование, и то я в процессе слишком часто чувствовал себя имбецилом (особенно пока читал Джианолу).
Нет ни заказчика на этот волшебный инструмент, ни исполнителей. Иначе хотя бы Идрис допилили до хоть какого-нибудь состояния, похожего на «готов к продакшену в разумных пределах».
Нет ни заказчика на этот волшебный инструмент, ни исполнителей. Иначе хотя бы Идрис допилили до хоть какого-нибудь состояния, похожего на «готов к продакшену в разумных пределах».
Ну там в хаскеле что-то шевелится на тему dependent haskell. Может, придём к готовому к проду завтипизированному языку с хорошим компилятором, просто с другой стороны. Пропозалы крутятся, завтипы мутятся.
Правда, учитывая скорость принятия (маленькую) и скоуп (ещё меньше, по пропозалу на каждую пердюшку в синтаксисе), придём туда мы году к 2050-му, не раньше.
Поэтому я пошел на некоторое количество соглашений с совестью и чувством прекрасного. Я не стремлюсь сделать полностью математически корректно. На границе линковки с другим BEAM-кодом — по-прежнему всё можно сломать, как в похапе.
Но зато я уже сейчас, на полуживом компиляторе, могу генерировать BEAM, которые внутри себя худо-бедно верифицированы. И линковать их снаружи, из больших проектов на эликсире и эрланге. Мне показалось важнее сделать что-то, чем можно пользоваться, и что представляет более внятные гарантии, в сравнении с динамической типизацией стандартной BEAM-машины.
Вот уж от кого я нейровысера не ожидал…
Обычные типы говорят: «это целое число». Зависимые типы говорят: «это целое число больше нуля и меньше длины списка».
Возможно я что-то путаю, но по-моему это называется refinement type (Как в Liquid Haskell) a не dependent type
Refinement type — это `type Positive = {i: Int | i > 0}`. Такие есть во всех недоязыках, претендующих на корректную имплементацию типов.
Dependent type — это типы, которые зависят от других типов, например `Vector(T, n)`, где T — тип, а n — переменная типа, которая может проникать в рантайм: def length(v: Vector(T, n)): Nat = n (пример из стандартной библиотеки: https://github.com/am-kantox/cure-lang/blob/main/lib/std/vector.cure#L14).
Refinement type — это
type Positive = {i: Int | i > 0}.
Плюс движок для работы с refinement'ами, чтобы Positive спокойно передавалось в функцию, ожидающую NonNegative . В этом основной смысл RT — можно сэкономить на доказательствах, которые спокойно дисчарджатся солвером.
Такие есть во всех недоязыках, претендующих на корректную имплементацию типов.
Можно весь список плз? Потому что мне известно очень мало таких языков — по большому счёту из более-менее готовых к проду это LH и F*.
Dependent type — это типы, которые зависят от других типов
От других термов.
Зависимость от других типов — это простой параметрический полиморфизм, бастардизированная версия которого есть даже в плюсах.
n— переменная типа
В нормальных завтипизированных языках это обычный терм.
У вас можно считать n из файла (или из сети) в рантайме обычной функцией toNat . readFile, получить вектор соответствующей длины (считав его тоже из файла, или replicate : (n : ℕ) → a → Vect n a) и что-то с ним сделать?
Так-то в хаскеле тоже есть DataKinds, но есть некоторые причины, почему он не завтипизированный.
переменная типа, которая может проникать в рантайм
В 2025-м ожидаешь, что это можно контролировать. Например, ИМХО самая доступная статья на тему — https://dl.acm.org/doi/pdf/10.1145/3408973
У вас можно считать
nиз файла (или из сети) в рантайме
Нет. И я не могу пока понять, зачем.
А вот за это — нечеловеческое спасибо.
Можно весь список плз?
Мы же не первый год знакомы, вы все еще наивно полагаете, что я в публичном пространстве — не умножу любую сущность на миллион?
Плюс движок для работы с refinement'ами […]
Я пока на стадии принятия. Я решил, что мне будет проще (по крайней мере, на первых порах) поддерживать код, в которых NonNegative будет дисчарджиться разработчиком.
И зачем завязываться на SMT-солверы? Может быть какие-то вещи они доказать не осилят, и придется доказывать на Coq Rocq или чем-то подобном? Насколько я помню, Frama-C переводит свои ASCL-контракты в WhyML, и там он может быть оттранслирован в кучу разных автоматических и интерактивных пруверов https://www.why3.org/#provers. Может быть вам тоже стоит использовать такой подход?
Я тщательно рассматриваю пулл-реквесты.
Ну так WhyML далеко не всесилен и может разве что тактики подобрать, полное доказательство - это уже вручную. А Z3/CVC - хорошо, много лучше, чем ничего, но не идеал. Но идея, конечно, хорошая. Правда, если кому-то реально нужно, возьмет Lean4 с завтипами и HoTT(вроде бы) + будет иметь уже готовый к пуску бинарь. А Frama очень многого не поймет в простом сишном коде, афаир, уж проще сразу Isabelle/C или Autocorres :)
Какой еще бинарь? Нахрена мне бинарь? Что непонятного в постановке задачи:
компилироваться в BEAM и прозрачно линковаться с эрлангом, эликсиром, глимом и даже лфе
Я понимаю, что вы, наверное, погуглили ключевые слова, чтобы выглядеть поумнее, но я впервые слышу о том, что Lean4 способен верифицировать FSM, а при чем тут HoTT — вообще загадка.
Ну кстати возможно, что было бы интересно не только байткод для BEAM поддерживать, а иметь несколько таргетов (возможно, в виде простой генерации кода для Java/C++), потому что в программе вполне часто получается, что есть и какой-то стрёмный код который трогать не хочется, и какая-нибудь подсистема, которую наоборот хочется сделать максимально строгой и верифицируемой.
P.S. Прекрасно вас пойму, если будете поддерживать только BEAM, потому что много таргетов поддерживать сложнее.
Не получится, придётся всё, что за парсером и тайп-чекером — с нуля переписать. Да даже тайп-чекер: уже неясно, как реализовывать для нескольких голов функции, например. Но это бы и ладно.
Генерация кода — тупиковый путь, у меня не случайно свой компилятор: сгенерированный байт-код уже не подвергнется насилию со стороны умного компилятора, а код — запросто, и я навскидку не могу сказать, не испортит ли это гарантии (кажется, что не должно, но доказать за минутку я не умею).
Можно было бы подумать про генерацию AST, но Java/C++ — не умеют на уровне языка работать с AST.
А самое главное — передо мной совершенно другая задача: у меня есть экосистема, в которой меня устраивает всё, кроме отсутствия верификации. Акторную модель мне с собой предлагаете нести в C++? Работать с Akka в Java — ну ёлки, это вообще сторонняя библиотека.
Я не хочу захватить мир, я хочу облегчить жизнь себе и тем людям, которые выбрали отказоустойчивость, параллелизм и горизонтальное масштабирование из коробки.
Начали за здравие, а закончили нейроподелкой...
Зарегистрируйтесь на Хабре, чтобы оставить комментарий
Cure :: Завтипы и формальная верификация для BEAM