flang
Язык, в котором функция несёт свои тесты и обещания, а компилятор доказывает, что она завершается и держит обещания. Проверка — прямо в браузере.
Нажмите «Проверить». Первая проверка скачает компилятор flang 0.7.32 со страниц языка — около 10 МБ, дальше он берётся из кеша. Текст программы остаётся во вкладке.
Язык за минуту
flang — язык со словесным синтаксисом. Функция в нём несёт свои тесты
(пример) и обещания (обеспечивает, требует), а компилятор проверяет их до
запуска:
- завершение — у функции с пометкой
тотальнаякомпилятор доказывает, что она заканчивается на любом входе; - примеры —
flang checkвычисляет каждыйпримери падает, если ответ не совпал; - обещания —
flang check --proofдоказывает постусловие для всех входов или прямо говорит «не доказано»; - печать —
flang emitпревращает программу в исходник на C, Go, Rust, Python, Java, C#, Elixir, JavaScript или TypeScript.
модуль «Скидки»
тотальная функция «Скидка»
принимает сумма: неотрицательное
возвращает неотрицательное
обеспечивает «скидка не больше суммы» результат не больше сумма
пример «крупный заказ»
дано сумма равно 12000
ожидается 500
если сумма не меньше 10000
то 500
иначе 0Здесь компилятор вычислит пример, докажет, что функция завершается, и
докажет обещание «скидка не больше суммы» для любой суммы: в ветке то
он знает, что сумма не меньше 10 000, а значит не меньше 500.
Установка
Одна команда: скрипт ставит flang 0.7.32 в ~/.local/bin и сверяет архив с SHA256SUMS выпуска. Компилятор C и sudo не нужны.
curl -fsSL https://raw.githubusercontent.com/digitable-lol/flang/main/install.sh | shИли через Homebrew:
brew install digitable-lol/tap/flang-packageflang check file.flang | разбор, типы, завершение, примеры |
flang check file.flang --proof | то же плюс доказательство обещаний |
flang run file.flang --function «Total» | вычислить функцию и напечатать значение |
flang emit file.flang --target go | напечатать программу на другом языке |
flang | интерактивная оболочка |
Запасной путь: сборка из исходников выпуска 0.7.32 (нужны компилятор C и make)
curl -fsSLO https://github.com/digitable-lol/flang/releases/download/v0.7.32/flang-0.7.32-c.tar.gz
mkdir flang && tar -xzf flang-0.7.32-c.tar.gz -C flang
make -C flang
./flang/flang check program.flang --proofКаталог установки меняет PREFIX, версию — FLANG_VERSION. Остальные способы — asdf, пакеты deb и rpm — в описании установки.
Куда дальше
Справочник конструкцийКаждая конструкция с примером, который проверен компилятором и открывается в песочнице.
Практикум8 заданий с проверкой в браузере: от первой функции до доказательства индукцией.
Курс по языкуПятнадцать глав: синтаксис, типы, тотальность, библиотека, печать в другие языки.
Журнал измененийЧто менялось от выпуска к выпуску.
Библиотеки на flangТри библиотеки, написанные на языке целиком.
Документация языкаПолное описание на сайте flang.