Как учить язык дальше

Это порядок чтения: восемь шагов от установки до своей первой настоящей программы. У каждого шага сказано, что вы после него умеете, какую страницу читать и какой командой проверить, что шаг взят. Порядок не обязателен, но он выведен из того, чем одно опирается на другое: третий шаг не читается без второго.

Дорога: что за чем

1. Поставить

После шага: команда flang отвечает на --version.

Читать — Установка. Путей четыре; самый короткий — одна команда Homebrew, без Node и без сборки исходников.

flang --version

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

После шага: вы написали файл, проверили его и запустили функцию.

Читать — Первая программа. Там та же пятиминутка, что на главной, но подробно и до печати программы в C.

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

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

3. Учебник — шесть глав

После шага: вы понимаете, почему нет циклов, чем разбор отличается от свёртки и что именно обещает слово тотальная.

Читать — Учебник. Шестая глава доводит до утверждения, принятого ядром доказательств; на ней стоит остановиться и не спешить дальше.

Три привычки, которые здесь придётся отложить, и это главное содержание шага:

привычка	что вместо неё
цикл	свёртка или рекурсия
изменить элемент на месте	построить новое значение
бросить исключение	вернуть отказ значением

4. Своя задача

После шага: вы написали программу, которую не списали.

Возьмите задачу, которую уже решали на другом языке — факториал, Фибоначчи, проверку палиндрома, — и напишите её заново словами flang, с примером внутри каждой функции.

Если проверка отказала словом FLANG_NOT_TOTAL — это не поломка, а разговор: компилятор не увидел, почему рекурсия кончается. Что он принимает за убывание, разобрано в Что даёт признак «тотальная».

5. Справочник — когда дорожка кончилась

После шага: вы находите нужную форму записи, не спрашивая никого.

Справочник конструкций — все формы языка подряд;
Операции языка — «у меня список, нужна сумма без повторов — чем»;
Словарь языка — 150 понятий, из них 133 открыты на всех четырёх поверхностях записи;
Четыре поверхности записи — почему одно и то же пишется русскими словами и английскими.

6. Что доказывается, а что нет

После шага: вы отличаете доказанное от прогнанного и не путаете одно с другим.

Это середина языка, и здесь стоит задержаться дольше всего.

Что доказано, а что нет — граница проведена явно;
Зачем и как — двенадцать решающих правил ядра, каждое читается целиком;
Ядро отказало: чья это ошибка — все отказы ядра поимённо: какие правятся теоремой, а какие упираются в предел языка;
Разборы настоящих случаев — что это дало на живом коде.

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

7. Разговор с миром

После шага: вы понимаете, откуда в чистом языке берутся файлы, сеть и время.

Программа на flang не делает действий — она возвращает их описания, а исполняет их тот, кто программу запустил. Из этого вырастает всё остальное:

Базы данных — PostgreSQL: что написано и где границы;
Процессы, надзор, распределённость — несколько процессов, перезапуск упавшего, узлы на разных машинах.

8. Наружу: печать, встраивание, пакеты

После шага: ваша программа работает внутри чужой системы.

Как встроить flang в чужую программу — одна программа печатается в девять языков: c, cpp, csharp, elixir, go, java, js, python, rust;
Как писать пакеты — как отдать написанное другим;
Известные ограничения — прочитать до того, как упрётесь.

Если застряли

Компилятор отвечает не «ошибка», а именем беды и разбором:

flang check файл.flang         # что не сошлось
flang check файл.flang --proof # что именно доказано, а что нет
flang --help                   # двенадцать команд и что каждая делает

Отказ начинается с имени: FLANG_TYPE, FLANG_NOT_TOTAL, FLANG_PROOF_INDUCTION_STEP. Имена, которые начинаются с FLANG_PROOF_, — это отказы ядра доказательств, и они разобраны поимённо на странице Ядро отказало: чья это ошибка. Остальные названы в man flang, раздел ДИАГНОСТИКА.