flang

A language where a function carries its own tests and promises, and the compiler proves that it terminates and keeps them. Checks run right in the browser.

flang 0.7.32

Press «Check». The first check downloads the flang 0.7.32 compiler from the language site — about 10 MB, cached afterwards. Your program stays in the tab.

The language in a minute

flang is a language with a word-based syntax; its keywords are Russian words. A function carries its own tests (пример) and promises (обеспечивает, требует), and the compiler checks them before anything runs:

termination — for a function marked тотальная the compiler proves it finishes on every input;
examples — flang check evaluates every пример and fails if the answer differs;
promises — flang check --proof proves a postcondition for all inputs or says plainly that it is not proved;
output — flang emit turns the program into C, Go, Rust, Python, Java, C#, Elixir, JavaScript or TypeScript source.

модуль «Скидки»

тотальная функция «Скидка»
  принимает сумма: неотрицательное
  возвращает неотрицательное
  обеспечивает «скидка не больше суммы» результат не больше сумма
  пример «крупный заказ»
    дано сумма равно 12000
    ожидается 500
  если сумма не меньше 10000
    то 500
    иначе 0

The compiler evaluates the example, proves the function terminates and proves the promise «скидка не больше суммы» (the discount never exceeds the total) for every total: in the то branch it knows the total is at least 10 000, hence at least 500.

Install

One command: the script puts flang 0.7.32 into ~/.local/bin and verifies the archive against the release SHA256SUMS. No C compiler or sudo needed.

curl -fsSL https://raw.githubusercontent.com/digitable-lol/flang/main/install.sh | sh

Or with Homebrew:

brew install digitable-lol/tap/flang-package

`flang check file.flang`	syntax, types, termination, examples
`flang check file.flang --proof`	the same plus proving the promises
`flang run file.flang --function «Total»`	evaluate a function and print the value
`flang emit file.flang --target go`	print the program in another language
`flang`	interactive shell

Fallback: build from the 0.7.32 release sources (needs a C compiler and 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 changes the install directory, FLANG_VERSION the version. Other ways — asdf, deb and rpm packages — are in the installation guide.

Where next

Construct referenceEvery construct with an example that is checked by the compiler and opens in the playground. Practice8 tasks checked in the browser: from a first function to a proof by induction. The language courseFifteen chapters: syntax, types, totality, the library, output in other languages. ChangelogWhat changed from release to release. Libraries in flangThree libraries written entirely in the language. Language documentationThe full description on the flang site.

What’s new

Easier now0

flang

The language in a minute

Install

Where next