О языках с выразительными системами типов обычно говорят: "Если оно проверяет типы, то, вероятно, всё работает". Это происходит, в частности, с чистыми функциями с полиморфными типами -- тут в итоге получается столь мало вещей, которые можно сделать с каждым входом, что иногда единственная разумно выглядящая функция, которую удаётся написать, и становится единственно верной. То есть, в некоторых случаях можно просто сгенерировать функцию из сигнатуры типа.

Например, есть такая штука, как джанглоид -- кусочек кода, который синтезируется автоматически и выполняет некоторый условно клиентский запрос к API на основании заданных типов входных и выходных значений. Так вот, формальная теория джанглоидов была разработана в начале 2000-х, задолго до явления хипстерских AI-ассистантов. Джанглоиды отлично комбинируются, и на их основе для Eclipse (основной Java IDE того времени) был разработан плагин, который выдавал адекватные подсказки и варианты кода, и, в частности, нашёл решение 18 из 20 задач.
"Jungloid mining: helping to navigate the API jungle"

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

Но есть важный и контринтуитивный нюанс в понятии "чётко описывать типы". Этот момент тоже разбираем в СИ, потому что чем конкретнее тип, тем, парадоксальнее, большее количество реализаций он допускает. И наоборот, чем больше тип -- "дженерик", чем более он абстрактный, тем меньшее количество реализаций возможно.

=

Духовным наследником джанглоидов стал красивый проект SyPet

"SyPet will automatically find a sequence of API calls from these Java libraries that will pass all test cases provided by the programmer. "
но к сожалению тоже заброшен 5 лет назад.

Затем эти алгоритмы были расширены на полиморфные типы: проект Hoogle+, автоматическая генерация программы на Haskell на основе их сигнатур.
hoogleplus.goto.ucsd.edu
hoogle_plus