Comments 60
За попытку +.
По делу:
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
А, в этом смысле. Нет.
Меня Брэди покорил именно этим примеров в своей книжке, но я до сих пор не понимаю, зачем оно нужно в реальной жизни.
У меня на балконе растет гранат и перец, а не роза. Я никогда не сталкивался с примерами, когда оно действительно нужно. Но у меня кругозор — так себе.
но я до сих пор не понимаю, зачем оно нужно в реальной жизни.
Один из вариантов — таки типобезопасный printf. Вон, плюсисты нетривиально приседают, чтобы в std::fmt (или как его там, не игрался на практике с этой частью новых плюсов) известные в компилтайме строки позволяли проверять типы аргументов. В шланге и gcc добавили проверки (и аннотации для кастомных строк), чтобы проверять соответствие строки формата аргументам у обычного сишного printf. Наверное, это нужно.
Другой вариант из личной практики, когда я по фану делал на идрисе обёртку вокруг постгреса — можно описать структуру таблицы обычным языком термов, и потом обычными функциями Schema → Type создать что тип, значения которого соответствуют схеме, что все эти обёртки над create table / insert / update / etc.
В мейнстримных языках для этого обмазываются какой-нибудь рефлексией, и всё даёт нечитаемые ошибки и разваливается (в рантайме, если рефлексия — рантайм).
в
std::fmt[…] Наверное, это нужно.
Вы все время забываете (намеренно игнорируете) то, что я не хочу построить язык общего назначения. Можно сказать, что добавляю «верификационный сахар» в существующие и использующиеся эликсир/эрланг.
Я сознательно не хочу реализовывать всё правильно, «как надо». Во-первых, я не смогу, мне не хватит остатков образования. Во-вторых, мне нужен рабочий прототип вчера, а не план на 2037.
[…] обёртку вокруг постгреса […]
В мейнстримных языках для этого обмазываются какой-нибудь рефлексией […]
У меня в эликсире есть очень хорошие макросы, если мне втемяшится сделать что-то похожее, я нагенерирую весь этот код в процессе компиляции, с правильными рантайм-проверками с адекватными сообщениями (или компайл-тайм проверками, если надо, обернув каждый терм в структуру, которую умеет понимать компилятор).
Конкретно этот тип доказательного програмирования я при этом считаю бессмысленным. А в языке, который я пишу (надеюсь, пока) в одно рыло, — мой голос сука решающий.
Да какое нафиг ℕ на машинах с конечной памятью, о чём вы? Речь может идти только о кольце остатков по модулю (Zm), а в этом случае всё хорошо доказывается.
Обычное ℕ. На машинах с конечной памятью (и в тетрадках с конечным числом листов) вы вполне себе можете доказывать вещи про бесконечный ℕ.
И это на самом деле полезно, потому что как-то очень глупо перепроверять все доказательства и ждать 2^100500 времени после того, как вы просто купили железку с памятью чутка побольше.
Речь может идти только о кольце остатков по модулю (Zm), а в этом случае всё хорошо доказывается.
И, кстати, совсем забыл: там ещё доказывается, что ∃ n. n + 1 = 0, что неверно для натуральных чисел. Поэтому, короче, это очень вредная модель.
Да нет, модель как раз крайне полезная. Примерно всё вокруг вас посчитано с её помощью.
А вот где на практике нужна мощность натуральных чисел за пределами Zm с технически доступным модулем — я представить не могу.
Я на всякий случай уточню: вы правда не понимаете, что доказательства могут быть не только про тот диапазон чисел, чем я считаю сдачу в магазине?
за пределами Zm с технически доступным модулем
Проверка тотальности через прямой перебор состояний не доступна ни для какого полезного на практике в более чем полутора приложениях m.
не доступна ни для какого полезного на практике
Булевы значения вышли из чата.
Ну для начала, на практике всё-таки обычно программисты работают с частично-рекурсивными функциями, и при нормально написанных предусловиях контракта (автор для этого пытается использовать завтипы, но это не единственный способ) полный перебор 2^64 комбинаций каждого параметра — это немножко overkill.
Во-вторых, арифметика остатков примерно такая же, как и арифметика натуральных чисел. Там есть свои тонкости с целочисленным переполнением, например, или с кривым делением на 0 в х86, но в целом — примерно такая же по сложности с точки зрения автоматического доказательства теорем.
Теоретически - да. Практически - разницы нет, пара вложенных циклов по bigint уже превышает время жизни вселенной на порядки
Так задача вроде не выполнить цикл, а доказать, что он не выполнится.
Просто как бы куча различных линтеров и компиляторов именно этим и занимаются, в т.ч. умеют детектировать бесконечные циклы
Зачем коллаца? Рассмотрим какую-нибудь сортировку. Вот например такая реализация на Haskell:
bubbleSort :: Ord a => [a] -> [a]
bubbleSort = untilFixed bubblePass
where
bubblePass [] = []
bubblePass [x] = [x]
bubblePass (x:y:xs)
| x > y = y : bubblePass (x:xs)
| otherwise = x : bubblePass (y:xs)
untilFixed f x = let fx = f x
in if fx == x then x else untilFixed f fx
Такой код может быть переписан на STMLib относительно легко
(set-logic ALL)
(set-option :produce-models true)
; bubblePass :: [Int] -> [Int]
; Haskell:
; bubblePass [] = []
; bubblePass [x] = [x]
; bubblePass (x:y:xs)
; | x > y = y : bubblePass (x:xs)
; | otherwise = x : bubblePass (y:xs)
(define-fun-rec bubblePass ((s (Seq Int))) (Seq Int)
(ite (<= (seq.len s) 1)
; [] или [x]
s
; (x:y:xs)
(let ((x (seq.nth s 0))
(y (seq.nth s 1))
(len (seq.len s)))
(let ((xs (seq.extract s 2 (- len 2))))
; tailInput = if x > y then (x:xs) else (y:xs)
(let ((tailInput
(ite (> x y)
(seq.++ (seq.unit x) xs)
(seq.++ (seq.unit y) xs))))
; tailOutput = bubblePass tailInput
(let ((tailOutput (bubblePass tailInput)))
; head = if x > y then y else x
; результат: head : tailOutput
(seq.++ (seq.unit (ite (> x y) y x))
tailOutput)))))))
; untilFixed :: (a -> a) -> a -> a
; Haskell-специализация:
; bubbleSort = untilFixed bubblePass
(define-fun-rec untilFixed ((s (Seq Int))) (Seq Int)
(let ((fx (bubblePass s)))
(ite (= fx s)
s
(untilFixed fx))))
(define-fun bubbleSort ((s (Seq Int))) (Seq Int)
(untilFixed s))
(define-fun initialArray () (Seq Int)
(seq.++ (seq.unit 9)
(seq.++ (seq.unit 2)
(seq.++ (seq.unit 4)
(seq.++ (seq.unit 1)
(seq.++ (seq.unit 3)
(seq.++ (seq.unit 5)
(seq.++ (seq.unit 7)
(seq.++ (seq.unit 8)
(seq.++ (seq.unit 6)
(seq.unit 0)
))))))))))
(define-fun sortedArray () (Seq Int)
(bubbleSort initialArray))
(check-sat)
(get-value (initialArray sortedArray))
Вроде всё корректно. Тут я для примера сортирую список 9 2 4 1 3 5 7 8 6 0. Можно запустить это в Z3 и он действительно сортирует, только он не сможет доказать, что такая сортировка работает для общего случая. Для проверки сортировки тут требуется функция для проверки упорядоченности (для любых двух соседних элементов a, b должно быть верно, что a <= b) и что массив после сортировки является перестановкой изначального массива, и что для любых списков любой длины эти оба условия выполняются. Если так сделать, Z3 просто зависнет или отвалится по таймауту. Такое надо через Rocq, Idris, Agda и прочие proof assistant доказывать
читаю профессиональные форумы
Это, например, какие?
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 будет дисчарджиться разработчиком.
Нет. И я не могу пока понять, зачем.
Считайте это тестом, что n — действительно обычный терм, а не костыль уровня DataKinds.
Я решил, что мне будет проще (по крайней мере, на первых порах) поддерживать код, в которых
NonNegativeбудет дисчарджиться разработчиком.
Так а что у вас SMT-то тогда делает? Большая часть практических применений RT сводится к тому, что для использования { ν : T | ρ } там, где ожидается { ν : T | ρ' }, достаточно проверить ρ ⇒ ρ', а это вполне себе решается солверами в значимой части практически полезных применений.
И зачем завязываться на 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 — ну ёлки, это вообще сторонняя библиотека.
Я не хочу захватить мир, я хочу облегчить жизнь себе и тем людям, которые выбрали отказоустойчивость, параллелизм и горизонтальное масштабирование из коробки.
Начали за здравие, а закончили нейроподелкой...
Мне бы хватило такого если б заморочился на раст написать макрос
refinement_type! {
PositiveUsize(u64) where |x| x > 0, "must be positive"
}Который разворачивался бы до
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub struct PositiveUsize(pub u64);
#[derive(Debug)]
pub struct PositiveUsizeError(pub &'static str);
impl std::fmt::Display for PositiveUsizeError {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
write!(f, "{}", self.0)
}
}
impl std::error::Error for PositiveUsizeError {}
impl PositiveUsize {
pub fn new(value: u64) -> Result<Self, PositiveUsizeError> {
if value > 0 {
Ok(PositiveUsize(value))
} else {
Err(PositiveUsizeError("must be positive"))
}
}
pub fn get(&self) -> u64 {
self.0
}
pub fn into_inner(self) -> u64 {
self.0
}
}А дальше что-то вроде From для проброса ошибок куда-то наверх типа контроллера. Вручную, но не сложно
def length(_v: Vector(T, n)): Nat = n гораздо нужнее.
struct Vector<T, const N: usize> {
data: [T; N],
}Или
impl<T, const N: usize> Vector<T, N> {
pub const fn length(&self) -> usize {
N
}
}Но только если число известно на стадии компиляции
Что-то сложнее только в рантайм
Арифметика complile time выглядела бы так
fn append<T, const N1: usize, const N2: usize>(
a: Vector<T, N1>,
b: Vector<T, N2>,
) -> Vector<T, { N1 + N2 }> // ← пока НЕ поддерживается в стабильном Rust
Cure :: Завтипы и формальная верификация для BEAM