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

Нужен только Node. Компилятор написан без единой внешней зависимости — это не принцип, а требование: язык, который не собирается без интернета, бесполезен ровно тогда, когда нужен.

git clone https://github.com/digitable-lol/flang.git
cd flang

Всё дальше работает сразу — ставить ничего не надо.

Проверить, что всё на месте

node flang/bin/flang.mjs version

Написать программу

Положите в файл privet.flang:

модуль «Привет»

тотальная функция «Удвоить»
  принимает н: число
  возвращает число
  обеспечивает результат равно (2 умножить на н)
  пример «Дважды два»
    дано н равно 2
    ожидается 4
  н плюс н

Здесь пять вещей, и каждая делает свою работу:

• **тотальная — обещание, что функция завершается на любом входе. Компилятор его проверяет** и откажется собирать файл, если доказать не сможет.
• **принимает / возвращает** — типы. Проверяются статически.
• **обеспечивает — постусловие: что верно про результат. Не для всех входов, которые вы придумали, а для всех вообще**, если ядро сумеет это доказать.
• **пример** — исполняемый пример. Он часть программы, а не тест сбоку, и прогоняется при каждой проверке.
• последняя строка — тело.

Проверить

node flang/bin/flang.mjs check privet.flang

Проверяются сразу: типы, завершаемость, примеры. Ответ приходит в JSON — это машинный вход, и он же читается глазами.

Проверить с доказательствами

node flang/bin/flang.mjs check privet.flang --proof --pretty

Здесь начинается то, ради чего язык существует. Ядро попробует доказать постусловие — то есть показать, что оно верно на всех входах, а не только на двойке из примера.

Ответ скажет одно из трёх, и разница между ними существенна:

• доказано ядром — утверждение верно про все входы;
• на сетке — нарушений не нашли, прогнав по значениям. Это не доказательство, и ведомость говорит это прямо;
• объявлено, не доказано — ядру не хватило правил. Утверждение при этом считается во время работы, на тех входах, которые придут.

Запустить

node flang/bin/flang.mjs run privet.flang --function «Удвоить» --args '{"н": 21}'

Напечатать в другой язык

node flang/bin/flang.mjs emit privet.flang --target c --out ./вывод

Целей семь: c, go, rust, python, java, csharp, elixir. Напечатанный код обязан выдавать те же значения и те же коды ошибок, что интерпретатор — это проверяется побайтово на всём корпусе, а не декларируется.

Попробовать вживую

node flang/bin/flang.mjs repl

Что дальше

• Зачем доказательства и как они устроены
• Спецификация языка — что в нём есть