Зачем это нужно

Здесь правило написано один раз и в той форме, которую читает человек из предметной области, а не только программист (фрагмент examples/library-api/lib/fine.flang):

объект «Просроченная выдача»
  «дней просрочки»: число
  «книга редкая»: признак

тотальная функция «Рассчитать штраф»
  принимает «выдача»: «Просроченная выдача»
  возвращает число
  обеспечивает «Штраф ограничен» результат не больше 500
  пример «Вернули вовремя»
    дано «выдача» равно (запись «Просроченная выдача» с «дней просрочки» равным 0 и «книга редкая» равным нет)
    ожидается 0
  пример «Две недели и редкая книга»
    дано «выдача» равно (запись «Просроченная выдача» с «дней просрочки» равным 14 и «книга редкая» равным да)
    ожидается 500
  пусть «дней» равно («выдача».«дней просрочки»)
  пусть «редкая» равно («выдача».«книга редкая»)
  пусть «за просрочку» равно если «дней» больше 0 то 50 иначе 0
  пусть «за долгую» равно если «дней» не меньше 14 то 150 иначе 0
  пусть «за редкую» равно если («редкая» равен да) и притом («дней» больше 0) то 300 иначе 0
  («за просрочку» плюс «за долгую») плюс «за редкую»

Ни фигурных скобок, ни стрелок, ни точек с запятой: поверхность отступная и словесная, а читаемые имена берутся в кавычки-ёлочки.

Три вещи здесь стоят рядом с телом функции и уезжают вместе с ним. Примеры — не тесты в соседнем файле, а часть объявления: flang test находит их сам. обеспечивает — обещание о результате на любом входе, а не на перечисленных. тотальная — признак, за который отвечает компилятор: он либо доказывает завершение сам (композицией, структурой или точным шагом по натуральному), либо требует, чтобы меру назвал автор (убывает), и тогда ставит сторожа НА ВРЕМЯ РАБОТЫ. Второе — не доказательство: flang check отвечает 0, а не убывшая мера валит программу отказом FLANG_MEASURE уже на прогоне. Чем несётся обещание у каждой функции, говорит flang check --proof; разбор — «Что даёт признак тотальная».

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

flang emit examples/library-api/lib/fine.flang --target python --out вывод

даёт в вывод/shtrafy.py, дословно:

    # постусловие «Штраф ограничен»
    if not rt.post(ctx, rt.lte(ctx, _t5, rt.number(500.0)), "Штраф ограничен", "Рассчитать штраф"):
        raise rt.fail("FLANG_PROPERTY", "нарушено свойство «Штраф ограничен» функции «Рассчитать штраф»")

FLANG_PROPERTY — собственный код языка, и формулировка сообщения тоже его. Служба на Python, служба на Go и бинарник на C, напечатанные из этой функции, откажут одному и тому же входу одними и теми же словами. Вот что «единый источник правды» обязан означать, чтобы чего-то стоить.