Подход "программы как устройства" с встроенной отладкой и мониторингом развивали несколько выдающихся специалистов: Дейкстра настаивал, что код и доказательство должны расти вместе — программу нельзя писать, а потом верифицировать, верификация должна быть встроена в процесс разработки. Он отвергал метод Хоара (постфактум-проверку) как непрактичный и требовал, чтобы корректность была частью конструкции программы, а не внешним инструментом.[microsoft] Хоар разработал логику Хоара для верификации структурированных программ через пре- и постусловия. Его Hoare State Monad — это монада состояния с предикатами для отслеживания состояния до и после вычислений, что позволяет встраивать проверки прямо в типовую систему. Это философия "программа = устройство с контрактами".[microsoft] Автор "Philosophy of Software Design" продвигает идею глубоких модулей (deep modules) — простой интерфейс скрывает сложную реализацию, но внутри должна быть возможность инспекции и отладки. Он критикует "tact