Спасибо за наводку с Dafny. Оба языка действительно реализуют подход Correct-by-Construction и используют общие ключевые слова requires/ensures/invariant. Но делают это по разному. Dafny полагается на математическое доказательство, а Orthon на архитектуру. для Orthon корректность это не конечная цель, а средство для других целей: комфорта человека и надёжной генерации кода моделями. Правильность достигается не доказательством произвольных свойств, а тем, что недопустимые состояния структурноневозможновыразить (Владение с move-семантикой, неизменяемость по умолчанию, алгебраические типы с исчерпывающим match, литеральные типы, Option/Result). Контракты есть, но занимают скромную нишу на втором ярусе инвариантов.
В Orthon корректность действительно встроена в конструкцию, но гарантировать можно только структурное соответствие, что код согласован со спецификацией, которая заявлена в самом коде. Компилятор здесь и есть статический анализатор, а семантическая модель задаёт инварианты, которые обязана выполнять любая реализация. Проверять поведенческое соответствие замыслу компилятор и не должен.
Полностью полагаться на систему типов я бы не стал. За счет типов корректность программы можно получить только частично. тип не решит проблемы в случае если функция возвращает (balance + amount) вместо (balance - amount).
Проектирую язык программирования Orthon. Систему проверка корректности распределяю по уровням. Каждый уровень ловит свой класс ошибок. Это рациональный компромисс.
Уровень 1 (система типов) - структурная корректность. Корректно типизированная программа не упадёт с ошибкой типа в рантайме. Нет null. Отсутствие зашито в Option и сужение типов превращает разыменование None в ошибку компиляции. match конструкция обязана покрывать все варианты. Это дёшево и проверяется целиком до запуска.
Уровень 2 (компилятор как анализатор) - корректность владения и мутации. Семантическая модель задаёт инварианты, которые обязана реализовать любая стратегия реализации: у каждого значения ровно один владелец; мутация требует исключительного доступа, чтение может быть общим; видимость не обходится в рантайме. Компилятор проверяет их статически - висячая ссылка или гонка на общем изменяемом состоянии становятся ошибкой сборки.
Уровень 3 (контракты сигнатур методов) - поведенческая корректность. Здесь живёт логика, которую типы не видят: Пример:
requires - предусловие (обязанность вызывающего). ensures - постусловие (гарантия метода). Где компилятор может доказать, будет ошибка компиляции. Остальное в debug/test-сборках становится проверками - requires как assert на входе, ensures как assert на выходе, - а в runtime пропускается.
Уровень 4 (типы с ограничениями) - корректность значений. Такая я же по сути идея:
type Age = Int requires v >= 0 && v <= 150
Ограничение объявлено один раз на типе и проверяется на каждой границе, где в тип входит значение. Сигнатура fn register(age: Age) уже несёт знание о допустимом диапазоне - без проверки в теле.
По коммиту/PR в master запускался gihub actions pipeline. Собирался докер образ и пушился в ECR. Затем через SSM запускалась команда - на EC2 выполнялся deploy.sh скрипт. Результаты запуска команды логировались в cloud-watch. Результаты вызова команды влияли на пайплайн на github. deploy.sh в свою очередь
- логировал процесс деплоя, - выкачивал .env и compose.yaml из AWS SSM Parameter Store если обновилилсь - обновлял docker образ и перезапускал compose сервисы
сам deploy.sh залетал на EC2 при инициализации инстанса. Инфраструктуру я подготавливал с помощью terraform. Нужна была схема деплоя попроще
столкнулся с похожей проблемой быстрого деплоя. решил ее созданием cli плагина для docker. https://github.com/webcane/docker-deploy сервис который хотим развернуть на удаленной машине представляет собой compose.yaml и при необходимости набор конфигов. хранится в git. меняем настройки локально, деплоим одной командой - docker deploy. Для vpn сервиса такой способ разворачивания тоже должен подойти
Как раз начал работать с библиотекой angular material design, поэтому когда заметил в браузере переход на новый дизайн, был приятно удивлен знакомой анимации.
Спасибо за наводку с Dafny. Оба языка действительно реализуют подход Correct-by-Construction и используют общие ключевые слова
requires/ensures/invariant. Но делают это по разному.Dafny полагается на математическое доказательство, а Orthon на архитектуру.
для Orthon корректность это не конечная цель, а средство для других целей: комфорта человека и надёжной генерации кода моделями. Правильность достигается не доказательством произвольных свойств, а тем, что недопустимые состояния структурно невозможно выразить (Владение с move-семантикой, неизменяемость по умолчанию, алгебраические типы с исчерпывающим
match, литеральные типы,Option/Result). Контракты есть, но занимают скромную нишу на втором ярусе инвариантов.В Orthon корректность действительно встроена в конструкцию, но гарантировать можно только структурное соответствие, что код согласован со спецификацией, которая заявлена в самом коде. Компилятор здесь и есть статический анализатор, а семантическая модель задаёт инварианты, которые обязана выполнять любая реализация. Проверять поведенческое соответствие замыслу компилятор и не должен.
используете ли Вы для описания контрактов стандарты, ODCS например?
https://martinfowler.com/articles/making-data-ready-for-agentic-ai.html
Полностью полагаться на систему типов я бы не стал. За счет типов корректность программы можно получить только частично. тип не решит проблемы в случае если функция возвращает (balance + amount) вместо (balance - amount).
Проектирую язык программирования Orthon.
Систему проверка корректности распределяю по уровням. Каждый уровень ловит свой класс ошибок. Это рациональный компромисс.
Уровень 1 (система типов) - структурная корректность. Корректно типизированная программа не упадёт с ошибкой типа в рантайме. Нет null. Отсутствие зашито в Option и сужение типов превращает разыменование None в ошибку компиляции. match конструкция обязана покрывать все варианты. Это дёшево и проверяется целиком до запуска.
Уровень 2 (компилятор как анализатор) - корректность владения и мутации. Семантическая модель задаёт инварианты, которые обязана реализовать любая стратегия реализации: у каждого значения ровно один владелец; мутация требует исключительного доступа, чтение может быть общим; видимость не обходится в рантайме. Компилятор проверяет их статически - висячая ссылка или гонка на общем изменяемом состоянии становятся ошибкой сборки.
Уровень 3 (контракты сигнатур методов) - поведенческая корректность. Здесь живёт логика, которую типы не видят: Пример:
requires - предусловие (обязанность вызывающего).
ensures - постусловие (гарантия метода).
Где компилятор может доказать, будет ошибка компиляции. Остальное в debug/test-сборках становится проверками - requires как assert на входе, ensures как assert на выходе, - а в runtime пропускается.
Уровень 4 (типы с ограничениями) - корректность значений. Такая я же по сути идея:
Ограничение объявлено один раз на типе и проверяется на каждой границе, где в тип входит значение. Сигнатура
fn register(age: Age)уже несёт знание о допустимом диапазоне - без проверки в теле.Похожая схема у меня была реализована в AWS.
По коммиту/PR в master запускался gihub actions pipeline.
Собирался докер образ и пушился в ECR.
Затем через SSM запускалась команда - на EC2 выполнялся deploy.sh скрипт. Результаты запуска команды логировались в cloud-watch.
Результаты вызова команды влияли на пайплайн на github.
deploy.sh в свою очередь
- логировал процесс деплоя,
- выкачивал .env и compose.yaml из AWS SSM Parameter Store если обновилилсь
- обновлял docker образ и перезапускал compose сервисы
сам deploy.sh залетал на EC2 при инициализации инстанса.
Инфраструктуру я подготавливал с помощью terraform.
Нужна была схема деплоя попроще
до 0. потребление у minipc 15Вт примерно
столкнулся с похожей проблемой быстрого деплоя. решил ее созданием cli плагина для docker. https://github.com/webcane/docker-deploy
сервис который хотим развернуть на удаленной машине представляет собой compose.yaml и при необходимости набор конфигов. хранится в git. меняем настройки локально, деплоим одной командой -
docker deploy. Для vpn сервиса такой способ разворачивания тоже должен подойтиспасибо за конструктивную критику. формат подачи поправил.