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

Пять шагов: написать файл, проверить его, прогнать примеры, запустить функцию, напечатать программу в C. Нужен установленный flang — как его поставить.

Всё, что стоит ниже в блоках вывода, — ответ настоящего прогона. Команды копируются подряд.

Написать

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

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

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

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

Имена — модуля, функции, примера — пишутся в ёлочках «…». Заменить их на " или ' нельзя: по ёлочкам разбор отличает придуманное вами имя от слова языка.

Вход объявлен неотрицательное, а не число, и это не мелочь. Объявите принимает н: число — и проверка откажет, потому что в типе число живёт «не число» (оно получается, например, из 0 делить на 0), а сравнивать его нельзя ни с чем:

FLANG_BOUND_ON_NAN в файле hello.flang, строка 6, столбец 3: постусловие
«удвоенное не меньше исходного» функции «Удвоить» ЛОЖНО, и контрпример назван:
«н» объявлен типом «число», а «не число» живёт в этом типе и стоит ВНЕ ПОРЯДКА
— оно не больше и не меньше ничего, включая самоё себя.
…

Отказ называет три починки; здесь выбрана первая — объявить вход отрезком неотрицательное. Вторая — предусловие требует «н не меньше нуля» н не меньше 0, за него платит вызывающий.

Проверить

flang check hello.flang

модуль «Привет»: функций 1, из них с доказанным завершением 1; типов 0
hello.flang: проверено — разбор, типы, завершаемость, ядро и примеры; замечаний нет

Код возврата 0. За одним словом check стоит пять работ подряд: разбор, типы, завершаемость, ядро доказательств, примеры. Остановка на любой из них означает, что печати не будет: непроверенное не печатается.

Ответ приходит по-русски, на какой бы поверхности вы ни писали. Слово из вашего файла компилятор цитирует ваше: английский файл получит в сообщении 'if', а не 'если'.

Прогнать примеры

flang test hello.flang

hello.flang: примеров 1, прошло 1, не прошло 0

Запустить

flang run hello.flang --function Удвоить --args '{"н": 21}'

42

Имя функции здесь без ёлочек: в объявлении они часть записи, в командной строке — уже нет.

--args берёт JSON-объект: ключ — имя параметра, как оно написано в принимает. Читается плоский объект скаляров — число, строка, true, false, null. Список так не передать:

flang run summa.flang --function Сумма --args '{"элементы": [1,2,3]}'

flang run: «--args» разобрать не удалось — ждался плоский объект скаляров, вроде '{"н":10}'

Код возврата 2. Как передавать список и запись — Операции языка, раздел про --args.

Типы аргументов flang run сверяет. Функция «Факториал» объявлена на неотрицательное, и на −3 отвечает так:

FLANG_TYPE: вызов функции «Factorial»: аргумент «n»: -3 вне неотрицательное

Что говорит отчёт о доказательствах

flang check hello.flang --proof

Ядро пробует доказать постусловие — показать, что оно верно на всех входах, а не только на двойке из примера. Про эту программу оно отвечает так:

чем несётся обещание «тотальная»:
  «Удвоить»  доказано композицией: рекурсии нет, обещание сложено из обещаний тех, кого зовёт

что высказано и чем это несётся:
  постусловие «удвоенное не меньше исходного» функции «Удвоить» — сетка 1 значение
  (примеры функции): нарушений НЕ ИСКАЛИ — прогона примеров не было, посчитано только
  их число. Это не доказательство — теоремы при утверждении нет

Три слова отчёта не взаимозаменяемы:

Как довести утверждение до «доказано» — в учебнике, глава 6.

Напечатать в C

flang emit hello.flang --target c --out ./вывод

напечатано файлов 6, байт 297459, в ./вывод
аргументы напечатанной программы по типам не проверяются: это ограничение двоичного flang, полная проверка есть в версии для Node
проверено перед печатью — разбор, типы, завершаемость и ядро доказательств.
ПРИМЕРЫ НЕ ПРОГНАНЫ: их считает вычислитель на самом языке, и на самых больших
программах он в предел шагов этого бинарника не укладывается — свяжи с ними
печать, и компилятор перестал бы печатать сам себя. Прогоните их отдельно:
flang test <файл>

Каталог вывода emit заводит сам. Собирается напечатанное обычным make:

make -C ./вывод

cc -std=c99 -Wall -Wextra -Werror -pedantic -O2 -flto   -c -o flang_runtime.o flang_runtime.c
cc -std=c99 -Wall -Wextra -Werror -pedantic -O2 -flto   -c -o privet.o privet.c
ar rcs libprivet.a flang_runtime.o privet.o
cc -std=c99 -Wall -Wextra -Werror -pedantic -O2 -flto   -c -o flang_cli.o flang_cli.c
cc -std=c99 -Wall -Wextra -Werror -pedantic -O2 -flto -o flang_cli flang_cli.o flang_runtime.o privet.o -lm -lpthread

Ни одного предупреждения при -Wall -Wextra -Werror -pedantic.

Одна ловушка: имя становится идентификатором целевого языка, и столкновение имён — отказ, а не тихое переименование. Назовите функцию «Double» — печати в C не будет вовсе:

flang emit: печать отказала — имена «Double» и «зарезервировано в целевом языке: double» дают один идентификатор «double» — переименуйте одно из них в модели

Отказ называет обе стороны столкновения, поэтому правка — одно слово в модели.

Печать в остальные цели

Целей печати девять: c, cpp, csharp, elixir, go, java, js, python, rust. Команда одна и та же:

flang emit hello.flang --target rust --out ./вывод-rust

напечатано файлов 7, байт 134520, в ./вывод-rust
…
собрать: cd <каталог> && cargo build, запустить target/debug/flang_cli <модуль>

Рядом с напечатанным лежат Makefile и Cargo.toml: собирается это cargo build, и получившийся flang_cli зовёт ту же функцию.

Что дальше

• Учебник — шесть глав от первой функции до утверждения, доказанного ядром
• Операции языка — что чем делается: списки, строки, числа