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

Тогда начни с того, что докажи это

А потом попробуй переформулировать это утверждение (доказательство будет повторено в точности) в хоть немного более общих терминах

Какое свойство отрезка приводит к этому?

Почему непрерывная в интервале (0; 1) функция 1/x своего наибольшего значения не достигает

Не понял. Ответы на то, каким именно образом реализовать невнятные требования, если повезёт, находятся в голове заказчика. Технически - да, это - в мире идей и программист их не видит. Но, кажется, это не то, что подразумевалось?

Небольшое обобщение 😊

Пусть X и Y – метрические пространства X \subset A и отображение f: A -> Y непрерывно на A. Тогда если A компактно, то f(A) тоже компактно.

Да да да, я именно прошу товарища увидеть идею компактности

Причем простейшее доказательство, скажем, через { f(x) >= последовательность сходящаяся к sup_[a..b] f } работает на любом компакте

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

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

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

У Линуса горело со спецификаций

https://yarchive.net/comp/linux/specs.html

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

Не нужно было лезть в голову заказчика, чтобы понять, что теорема Вейерштрасса про компактное А

Вот, согласен. Я это только называю постепенной формализацией требований.

Забавно. У меня обнаружено противоречие в нейронке, надо подумать

Указывается, что нисходящее программирование на достаточно полиморфном языке должно быть свободно от патологий абстракции?

А, тот аргумент все ещё держится, все правильно. Это программирование доказательством непротиворечивости спеки, оно свободно от указанной патологии, его проблема только в отсутствии прототипа, показывающего последствия спеки

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

Ну речь в данном случае о декларативных структурах с сильными типами

роб пайк, кен томпсон, керниган, фитцпатрик это макаки из гугла??