Цель flang — доказуемость, доступная обычному программисту

Языки, где программу можно доказать, существуют полвека: Coq, Agda, Idris, Lean. Все они требуют математической подготовки уровня диссертации, поэтому на них пишут доказательства, а программы для продакшена извлекают в OCaml или Haskell.

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

К версии 1.0.0 нужны: доказуемость, чистое ФП, строгая статическая типизация, отличная стандартная библиотека, отказоустойчивость в духе OTP, модульная система, распространение пакетов. Компилятор целиком на самом flang.

Чем ограничено. Это инженерная ставка, а не теоретическое открытие. За неё брались и отступали — см. condition-for-the-revolution о том, при каком условии она сыграет, и proven-is-not-correct о том, чего доказательство не даёт никогда.

Связано: what-is-deferred, owner-decisions