Всякая программная система, сколь бы сложной она ни была, есть в конечном счёте формальная теория некоторого фрагмента мира, материализованная в вычислительной среде. Это утверждение, тривиальное для философа, оказывается глубоко нетривиальным для инженера, ибо между формальной теорией и её материализацией пролегает пропасть семантический разрыв, порождаемый множеством трансляций: от неформальных требований к формальным спецификациям, от спецификаций к архитектурным моделям, от моделей к исполняемому коду, от кода к машинным инструкциям. Каждая трансляция есть потеря семантической точности, каждое преобразование это потенциальный источник дрейфа смысла. Традиционная инженерия программного обеспечения, какой бы изощрённой она ни была в инструментальном отношении, никогда не преодолевала этого разрыва; она лишь управляла его последствиями через тестирование, верификацию и непрерывную интеграцию, т.е. через процедуры, которые констатируют наличие ошибки, но не устраняют её онтологическую возможность. Читать далее