Рассуждения о вайбкодинге

В процессе чтения комментариев в одной статье на хабре я увидел среди них простой и важный.

Программа - не бинарная сущность.
Она не “работает или не работает”.

Ранее я обдумывал похожий вопрос, связанный с этим.
Вайбкодер в любом случае будет вынужден выяснить ограничения, связанные со своей конкретной задачей, если их нельзя получить извне.
И описать эти ограничения на формальном языке, если хочет, чтобы их можно было формально проверить.
Это вряд ли получится сделать, не зная формальные описания. А само описание будет в сущности кодом.
Вот этот момент - предельное описание поведения будет неотличимо от кода - мне кажется значимым.
Не для всех систем он очень важен, но он важен часто.

Вообще, при создании программы, кто формирует поведение и кто его контролирует?
Есть идея, что проблему контроля поведения можно тестами решить.
Однако, насколько должно быть описано поведения системы в этом случае?
Если например это функция с 1 параметром, и у этого параметра известен тип - то все более-менее очевидно.
Если тип неизвестен - уже начинаются сложности. В языках без строгой типизации придется проверять все типы данных и все варианты условий. И это только формальные проверки.
А если входящих параметров 2? Если например у нас будет 2 параметра, в каждом по 5 вариантов значений (пусть это будут enum или константы) - то чтобы однозначно проверить что все верно - нам понадобится 25 вариантов поведения функции описывать.
Сколько же параметров в реальных системах? Десятки, сотни. У каждого из них множество вариантов.
При описании мы полагаемся лишь на описывающего: он будет описывать взаимосвязи в очень большом пространстве вариантов, фактически вкладывая в описание результат работы своего мозга.

Так можем ли мы это формально однозначно проверить?

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

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

При наличии такого количества мест, где все может пойти не так - невольно можно задаться вопросом, а как вообще получается что машины код пишут?

Хорошо, что все типичные проблемы уже решены людьми. Остается только комбинировать готовые библиотеки и решения для реализации простых типичных задач.

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