Это всё прикладная мифология. В реальных проектах (ну, если судить по тому, что есть в открытом доступе), в этих доказательствах содержатся сотни аксиом, и как проверить, что в них нет ошибок? Про Lean вон любители Coq вообще говорят, что он неконсистентен, и что доверять его доказательствам нельзя. Ну, и т.д. и т.п. Серебрянной пули нет.

достаточно протестировать мозг, остальные тесты уже не потребуются))

Это-то давно известно: correct-by-construction programs, "make invalid states unrepresentable".

Это тоже прикладная мифология. Программу надо обкладывать максимумом доступных тестов и верификаций, чтобы минимизировать вероятность ошибки. Вне зависимости от качества мозга.

Я хотел сказать, что одних верификаций не достаточно, какой бы выразительной система типов ни была бы, ошибки возможны, и дополнительно обкладывать программу тестами целесообразно. Обратное тоже верно, если есть возможность что-то формально верифицировать, надо это делать.

да это так, шутейки, с тестами проблема в том, что их чаще пишут для галочки, чтоб тест покрывал основной кейс, на ревью тесты тяжело читать, особенно на pytest

Типы точно так же можно писать для галочки. Видел код на Haskell, по-моему, даже в каком-то компиляторе, где у большинства функций были сигнатуры только из Int-ов и String-ов

Но если заморочиться и написать по-уму, то гарантий и удобства немного больше, чем с тестами. 😊

грустно, на этом фоне у меня интересная идея возникла - часть запросов на проде, собирать в пакеты (запрос и полученные моки к нему) и перенаправлять в девелоп, с новыми фичами

да, и кажется это чекать на ревью проще, чем тесты

А вот это уже очень сильно зависит... 😔

не проще?

Сильно зависит. 🤷‍♀

качество программы стоит денег. если последствия ошибки. в проде стоят дешевле мер поввшения качества, зачем их принимать?

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

Проблема в том, что эксперт зачастую не умеет формализовать. Он умеет сказать: верно или не верно. И часто первой формализацией является сама программа, а не предварительно построенная логическая модель. И нужно учитывать, что во многих прикладных случаях модель записывается в дифф. уравнениях, minmax задачах, генеративных моделях. И кодировать это в формальных моделях сейчас просто не в чем... А в самом коде - ну вот как-то да получается.

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

так я и имею ввиду не эксперта в предметной области, а в задаче формализации. это пересекается, конечно.

и ничего плохого в том, что формализацией является программа - нет. зависит от квалификации эксперта.

эксперт же не идеальный объект

так и систему типов можно не прошивать, а навешивать

Вот я сомневаюсь... Типы - это синтаксическая концепция.

я сейчас не найду, но статьи такие есть