а по-моему оно называется "документация"

Да, кстати. Если бы нам хватало только лишь типов, мы бы вообще не писали документацию :)

Ну, это непростая задача, я согласен. Плавающий контракт означает, что программу можно понять так, а можно этак. Компилятор по факту(и в силу правил семантики языка) выбирает какой-то определенный путь, и выдает ошибку в соответствии с ним, хотя фактически ты мог иметь ввиду что-то совершенно иное(то есть пойти по иному пути). Фактически нам нужен более умный компилятор, который более глубоко способен понимать суть того, что ты пытался неявно выразить. Повторюсь, что это непростая исследовательская задача, но тут есть пространство для исследования, как мне кажется.

То есть у нас выбор между типами и документацией... хмм, что ж выбрать?

С типами получается всё хорошо только в узком подмножестве задач.

офк в тех япах где это так можно сделать: раст, хачкель, ..

Тут главное не пытаться общаться с любой достаточно сложной системой. Например, доки к winapi содержат требование, что если WM_INITDIALOG возвращает FALSE, то обработчик выставил фокус на потомка диалога. Не думаю, что подобное требование может быть записано системой типов раста или хаскеля

> Не думаю, что подобное требование может быть записано системой типов раста или хаскеля

Конечно может

а как это требование дальше стереть?

ну например вызвать функцию которая принимает IsChildFocused child и возвращает Not (IsChildFocused child)