Без заголовка

Я думаю что программирование-в-большом в основном сводится к проблеме спецификации и моделирования (софта). Т.е. к метапрограммированию. Ибо чтобы оперировать компонентами, нужно иметь их модели. Моделью для софтового компонета является спецификация (+ возможно какие-то знания об особенностях поведения, не включенные в спецификацию по той или иной причине, тем не менее они все равно специфицируют поведения, являются некоторой моделью). Ну а поскольку большими моделями оперировать тяжело, хочется чтобы это были формальные модели, и чтобы ими мог оперировать компьютер. В компьютер сайенс, кстати, накоплен весьма приличный опыт по части спецификации программ. Я могу отметить то с чем я столкнулся: 1. спецификации должны быть весьма подробными, ибо полезность простеньких спецификаций хоть и наличествует, но весьма ограниченна 2. спецификации должны быть обширными, потому как разные компоненты используют друг друга, ну и для всех желательно иметь спеки, иначе будут постоянно вылезать какие-то ограничения: не можем сделать то-то ибо нет спецификации для какого-то подкомпонента. Т.е. постоянно прерываешься на описание подкомпонентов. 3. обычные языки для спецификаций не годятся. Проблема состоит в том, что спецификаци фактически соответствует типу в языках программирования (т.е. программы, реализующие какую-то конкретную спеку, представляют собой тип). Но спецификации гораздо богаче типов в обычных языках. Значит, система типов должна быть весьма выразительной, чтобы её можно было использовать для специфкации. Такие типы называются dependent types. 4. Поскольку программа сама состоит из компонентов (всяких функций), то специфицированная программа есть программа сопровождаемая преобразованиями типов, т.е. преобразованиями спецификаци. Т.е. преобразованиями моделей. 5. Проверка соответствия программы спецификации называется верификацией программы. Ну есть еще всякие ограниченные версии проверок типа model checking и test generation. Ограниченные версии полезны, но всех проблем они не решают. Ибо там экспоненциальный рост вариантов, т.е. они применимы лишь на маленьких моделях. О масштабировании речь не идет.