TL;DR: Cure — это функциональный язык программирования для виртуальной машины BEAM (Erlang/Elixir/Gleam/LFE), который привносит математические доказательства корректности кода прямо во время компиляции. Используя SMT-солверы (Z3/CVC5), Cure проверяет типы зависимые от значений, верифицирует конечные автоматы и гарантирует отсутствие целых классов ошибок ещё до запуска программы.

---

Что такое Cure и зачем он нужен?

Проблема современной разработки

Без тестов не обойтись, но для некоторых критически-важных частей кода хотелось бы каких-нибудь более веских гарантий, например — доказательств корректности. При прочих равных, это не имеет смысла для интернет-магазинчиков и сайтов-визиток, но биржевая платформа, система управления беспилотником, или медицинское ПО — заслуживают чего-то посерьезнее тяп-ляп тестов.

При этом, все существующие языки, позволяющие доказывать корректность, — либо не готовы к продакшену, либо написаны инопланетянами для инопланетян, либо заставят вас весь остальной проект писать на тех же условиях (HTTP-запросу от пользователя проверка типов и гарантии корректности не нужны, а накладные расходы на них, такие, как время компиляции и само время написания — довольно значительные, чтобы ими пренебречь).

Я годами писал критические подсистемы на идрисе, переводил ручками на эликсир, и меня это устраивало — но ужасно раздражало. Да, при переводе (на любой границе с внешним миром) — математическая доказательность теряется, но это допустимый риск (для меня). Я точно знаю, что если «спайка» тщательно проверена, то код внутри будет работать как надо.

Но у идриса хватает своих проблем, я не считаю хаскелеподобный синтаксис приемлемым для взрослого программирования, да и переводить каждый раз туда-сюда — довольно муторно. И я подумал: а что, если написать свой язык, который будет компилироваться в BEAM и прозрачно линковаться с эрлангом, эликсиром, глимом и даже лфе?

Мне от языка-то надо всего-навсего три вещи:

• завтипы и солверы

• FSM в корке, со всеми плюшками

• отсутствие if-then-else

И я просто создал Cure.

Традиционный подход:

%% Erlang - проверки только во время выполнения
safe_divide(A, B) when B =/= 0 ->
    {ok, A / B};
safe_divide(_, 0) ->
    {error, division_by_zero}.

Да, это работает. Но что если вы забыли проверку? Что если логика усложнится и появится новый путь выполнения?

Подход Cure:

# Cure - математическое доказательство на уровне типов
def safe_divide(a: Int, b: {x: Int | x != 0}): Int =
  a / b
  
# Компилятор ДОКАЖЕТ, что b никогда не будет нулём
# Или программа не скомпилируется

Философия Cure

Cure стоит на трёх китах:

1. Верификация важнее удобства — когда корректность критична, синтаксический сахар вторичен

2. Математические доказательства вместо надежд — компилятор не просто проверяет типы, он доказывает свойства программы

3. BEAM как фундамент — вся мощь Erlang OTP, но с гарантиями корректности на уровне типов

---

Зависимые типы: Что это и зачем?

Простой пример

Обычные типы говорят: «это целое число». Зависимые типы говорят: «это целое число больше нуля и меньше длины списка».

# Тип зависит от ЗНАЧЕНИЯ
def head(v: Vector(T, n)): T when n > 0 =
  nth(v, 0)
  
# Компилятор ДОКАЖЕТ, что:
# 1. Вектор непустой (n > 0)
# 2. Индекс 0 всегда валиден
# 3. Результат имеет тип T

# Попытка вызвать head на пустом векторе?
# ❌ ОШИБКА КОМПИЛЯЦИИ

Реальный пример: безопасный доступ к списку

# Безопасный доступ - математически доказан
def safe_access(v: Vector(Int, n), idx: {i: Int | i < n}): Int =
  nth(v, idx)  # Без проверок - компилятор УЖЕ доказал безопасность!

# Использование
let my_vector = ‹5, 10, 15, 20›  # Vector(Int, 4)

safe_access(my_vector, 2)   # ✅ OK - 2 &lt; 4
safe_access(my_vector, 10)  # ❌ ОШИБКА КОМПИЛЯЦИИ - 10 &gt;= 4

Обратите внимание: никаких проверок в рантайме. Компилятор математически доказал, что idx всегда валиден. Это не просто «проверка типов» — это математическое доказательство.

---

SMT-солверы и формальная верификация

Что такое SMT-солвер?

SMT (Satisfiability Modulo Theories) — это математический движок, который проверяет, существует ли решение системы логических уравнений.

Представьте задачу:

Дано: x > 0, y > 0, x + y = 10
Вопрос: может ли x = 15?

SMT-солвер математически докажет, что нет — если x = 15, то y = -5, что нарушает условие y > 0.

Как Cure использует Z3

Cure интегрирует Z3 — самый мощный SMT-солвер от Microsoft Research — прямо в компилятор:

# Функция с гардами
def classify_age(age: Int): Atom =
  match age do
    n when n < 0 -> :invalid
    0 -> :newborn
    n when n < 18 -> :minor
    n when n < 65 -> :adult
    n when n >= 65 -> :senior
  end

Что делает компилятор с Z3:

1. Переводит гварды в SMT-формулы:

   (assert (< n 0))      ; первый case
   (assert (= n 0))      ; второй case
   (assert (and (>= n 0) (< n 18)))  ; третий case
   ...

2. Z3 проверяет полноту покрытия:

   • Все ли случаи покрыты?

   • Нет ли пересечений?

   • Нет ли недостижимых веток?

3. Гарантирует:

   ✓ Все целые числа покрыты
   ✓ Каждое число попадёт ровно в один case
   ✓ Нет мёртвого кода

Верификация конечных автоматов

FSM (Finite State Machine) — это сердце многих систем на BEAM. Я лично написал ажно целую библиотеку поддержки FSM с «верификацмями» на эликсире, но это, конечно, были костыли, сделанные из палок. В 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’ов), ② все состояния достижимы, ③ нет недоопределенных переходов, и ④ инварианты сохраняются. И всё это на этапе компиляции!

Пайпы

Я не пурист, я просто сделал пайпы монадическими. Подробнее вот тут.

---

Текущее состояние проекта

✅ Что работает (Версия 0.5.0 — Ноябрь 2025)

Полностью функциональная имплементация:

1. Компилятор (100% работоспособен)

   • Лексический анализ с отслеживанием позиций

   • Парсинг в AST с восстановлением после ошибок

   • Система зависимых типов с проверкой ограничений

   • Генерация байткода BEAM

   • Интеграция с OTP

2. Стандартная библиотека (12 модулей)

   • Std.Core — базовые типы и функции

   • Std.Io — ввод-вывод (в зачаточном состоянии, я не могу понять, нужен ли он мне вообще)

   • Std.List — операции со списками (map/2, filter/2, fold/3, zip_with/2)

   • Std.Vector — операции со списками определенной длины

   • Std.Fsm — работа с конечными автоматами

   • Std.Result / Std.Option — обработка ошибок

   • Std.Vector — индексированные векторы

   • И другие...

3. FSM Runtime

   • Компиляция FSM в gen_statem behaviors

   • Mermaid-нотация для FSM (State1 --> |event| State2)

   • Runtime операции (spawn, cast, state query)

   • Интеграция с OTP supervision trees

4. Оптимизация типов (25-60% ускорение)

   • Мономорфизация

   • Специализация функций

   • Инлайнинг

   • Устранение мёртвого кода

5. Гарды функций с SMT-верификацией

   def abs(x: Int): Int =
     match x do
       n when n < 0 -> -n
       n when n >= 0 -> n
     end
   # Z3 проверит полноту покрытия!

6. Интеграция с BEAM

   • [×] Полная совместимость с Erlang/Elixir

   • [ ] Hot code loading

   • [?] Distributed computing — кхм :) почти

   • [×] OTP behaviours

Не готово / не работает

• Type Classes/Traits — полиморфные интерфейсы (парсер готов, ждёт реализации)

• String interpolation — шаблонные строки

• CLI интеграция SMT — запуск Z3 из командной строки (API готов)

  ---

LSP и MCP: Разработка с комфортом

И это, внезапно, еще не все. Мне самому приходится довольно много возиться с кодом на Cure, поэтому параллельно разрабатываются полноценный LSP и MCP.

Language Server Protocol (LSP)

Cure поставляется с неплохим LSP сервером для IDE:

Возможности:

• Real-time диагностика — ошибки прямо в редакторе

• Hover информация — типы и документация по Ctrl+hover

• Go to definition — навигация по коду

• Code completion (пока довольно средняя)

• Code actions (всё, что может вывести солвер — из коробки)

• Type holes — _ для вывода типов (как дырки в идрисе)

Интеграция: Гипотетически, должно работать в любом редакторе с поддержкой LSP. Протестировано только в NeoVim.

Пример:

# Дырка                ⇓
def factorial(n: Int): _ =
  match n do
    0 -> 1
    n -> n * factorial(n - 1)
  end
  
# Hover покажет выведенный `Int`, а `<leader>ca` — вставит его по месту

Model Context Protocol (MCP)

Cure поддерживает MCP — новый протокол от Anthropic для интеграции с AI-ассистентами:

Что это даёт (для особо одаренных: список с эмоджиками — это контекстная шутка):

• ? AI-assisted coding — Claude/GPT понимает контекст проекта

• ? Умный поиск — семантический поиск по кодовой базе

• ? Type-aware рефакторинг — AI знает о типах

• ? Документация на лету — генерация docs из кода

Архитектура:

┌─────────────┐
│   Claude    │ ← MCP Protocol
│   /GPT      │
└──────┬──────┘
       │
┌──────▼──────────────┐
│   MCP Server        │
│  (Cure integration) │
├─────────────────────┤
│ • Code search       │
│ • Type queries      │
│ • Documentation     │
│ • Refactoring hints │
└─────────────────────┘

---

Как попробовать Cure

Установка

Требования:

• Erlang/OTP 28+

• Make

• Git

• (Опционально) Z3 для SMT-верификации

Шаги:

# 1. Клонируйте репозиторий
git clone https://github.com/am-kantox/cure-lang.git
cd cure-lang

# 2. Соберите компилятор
make all

# 3. Проверьте установку
./cure --version
# Cure v0.5.0 (November 2025)

# 4. Запустите тесты
make test
# ✓ All tests passed

Первая программа

Создайте hello.cure:

module Hello do
  export [main/0]
  
  import Std.Io [println]
  
  def main(): Int =
    println("Привет из Cure!")
    0
end

Скомпилируйте и запустите:

./run_cure.sh hello.cure
# Привет из Cure!

Примеры из коробки (они иногда ломаются)

# FSM: светофор
./cure examples/06_fsm_traffic_light.cure
erl -pa _build/ebin -noshell -eval "'TrafficLightFSM':main(), init:stop()."

# Работа со списками
./cure examples/01_list_basics.cure
erl -pa _build/ebin -noshell -eval "'ListBasics':main(), init:stop()."

# Pattern matching с гвардами
./cure examples/04_pattern_guards.cure
erl -pa _build/ebin -noshell -eval "'PatternGuards':main(), init:stop()."

# Обработка ошибок через Result
./cure examples/02_result_handling.cure
erl -pa _build/ebin -noshell -eval "'ResultHandling':main(), init:stop()."

---

Архитектура компилятора

Pipeline компиляции

┌──────────────┐
│  hello.cure  │ Source File
└──────┬───────┘
       │
       ▼
┌──────────────────┐
│   Lexer          │ Tokenization
│  (cure_lexer)    │ • Keywords, operators
└──────┬───────────┘ • Position tracking
       │
       ▼
┌──────────────────┐
│   Parser         │ AST Generation
│ (cure_parser)    │ • Syntax analysis
└──────┬───────────┘ • Error recovery
       │
       ▼
┌──────────────────┐
│  Type Checker    │ Type Inference
│(cure_typechecker)│ • Dependent types
│                  │ • Constraint solving
│  ┌─────────────┐ │
│  │ Z3 Solver   │ │ SMT Verification
│  │ (cure_smt)  │ │
│  └─────────────┘ │
└──────┬───────────┘
       │
       ▼
┌──────────────────┐
│  Optimizer       │ Type-Directed Opts
│(cure_optimizer)  │ • Monomorphization
└──────┬───────────┘ • Inlining
       │
       ▼
┌──────────────────┐
│  Code Generator  │ BEAM Bytecode
│ (cure_codegen)   │ • Module generation
└──────┬───────────┘ • OTP integration
       │
       ▼
┌──────────────────┐
│   Hello.beam     │ Executable
└──────────────────┘

Интеграция Z3

%% Упрощённый пример из cure_guard_smt.erl
verify_guard_completeness(Guards, Type) ->
    %% 1. Генерируем SMT формулы
    SMTFormulas = lists:map(fun guard_to_smt/1, Guards),
    
    %% 2. Проверяем покрытие
    Coverage = z3_check_coverage(SMTFormulas, Type),
    
    %% 3. Ищем пробелы
    case Coverage of
        complete -> 
            {ok, verified};
        {incomplete, Gap} -> 
            {error, {missing_case, Gap}};
        {overlapping, Cases} -> 
            {error, {redundant_guards, Cases}}
    end.

FSM компиляция

# Исходный FSM
fsm Light do
  Red --> |timer| Green
  Green --> |timer| Red
end

# Компилируется в gen_statem
-module('Light').
-behaviour(gen_statem).

callback_mode() -> state_functions.

red({call, From}, {event, timer}, Data) ->
    {next_state, green, Data, [{reply, From, ok}]}.

green({call, From}, {event, timer}, Data) ->
    {next_state, red, Data, [{reply, From, ok}]}.

---

Для чего Cure вообще не впёрся?

• Быстрое прототипирование (используйте Elixir)

• Веб-разработка общего назначения (Phoenix отлично справляется)

• Скрипты и glue code

• Проекты с частыми изменениями требований

Сравнение с другими языками

Философия проекта

Cure не пытается заменить Erlang или Elixir. Это специализированный инструмент для задач, где:

1. Корректность > Скорость разработки

2. Математические доказательства > Unit тесты

3. Compile-time гарантии > Runtime проверки

There are two ways of constructing a software design: One way is to make it so simple that there are obviously no deficiencies, and the other way is to make it so complicated that there are no obvious deficiencies. — Тони Хоар

---

Roadmap и будущее

Краткосрочные планы (2025–2026)

• [ ] Typeclasses/Traits — полиморфные интерфейсы

• [ ] CLI SMT integration — Z3 прямо из командной строки

• [ ] Улучшение LSP — code completion, refactoring

• [ ] Расширение stdlib — больше утилитарных функций

Среднесрочные (2026)

• [?] Effect system — трекинг эффектов как в Koka

• [ ] Package manager — управление зависимостями

• [ ] Distributed FSMs — верифицируемые распределённые автоматы

• [ ] Gradual typing — совместимость с динамическим Erlang

• [?] Macro system — compile-time метапрограммирование

Долгосрочное видение

Cure стремится стать языком выбора для критичных систем на BEAM:

1. Формальные методы становятся mainstream — не нишей для академиков, а стандартом индустрии

2. Математические гарантии на BEAM — reliability Erlang + correctness Cure

3. Инструментарий верификации — как сегодня unit тесты, завтра SMT-проверки

---

Ресурсы и ссылки

Документация

• Полуофициальная документация: /docs в репозитории

• Спецификация языка: docs/LANGUAGE_SPEC.md

• Руководство по типам: docs/TYPE_SYSTEM.md

• FSM: docs/FSM_USAGE.md

• Стандартная библиотека: docs/STD_SUMMARY.md

Примеры кода

• Базовые примеры: examples/01_list_basics.cure

• FSM демо: examples/06_fsm_traffic_light.cure

• Гарды и pattern matching: examples/04_pattern_guards.cure

• Зависимые типы: examples/dependent_types_demo.cure

Научные основы

• (этой книге я обязан существованием языка в принципе) Alessandro Gianola: «SMT-based Safety Verification of Data-Aware Processes»

• Z3 Solver: https://github.com/Z3Prover/z3

• SMT-LIB Standard: http://smtlib.cs.uiowa.edu/

• Idris tutorial: https://docs.idris-lang.org/

---

P.S. Частые вопросы

Q: Cure production-ready?
A: Компилятор функционален, stdlib работает, но проект молодой. Для критичных систем рекомендуется тщательное тестирование. Версия 1.0 ожидается в 2026.

Q: Нужно ли знать теорию типов?
A: Базовое использование не требует глубоких знаний. Для продвинутых возможностей (зависимые типы, SMT) желательно понимание основ.

Q: Совместим ли с Erlang/Elixir?
A: Да! Cure компилируется в BEAM bytecode и полностью совместим с OTP. Можно вызывать Erlang модули и наоборот.

Q: Почему не расширить Elixir вместо нового языка?
A: Зависимые типы требуют принципиально другой архитектуры компилятора. Добавить их в динамический язык невозможно без потери гарантий.

Q: Как быстро код на Cure?
A: Сопоставимо с Erlang. Оптимизации типов дают 25-60% ускорение. Zero runtime overhead от типов.

Q: Можно ли писать веб на Cure?
A: Возьмите Phoenix, напишите критические куски на Cure и слинкуйте BEAM из Elixir’а. Я сделаю этот процесс прозрачным для mix. В принципе, Cure имеет смысл использовать только для систем, где нужна верификация. Сайтег или приложулька прекрасно обойдутся без него.