OberonCore

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

В связи с доказательным программированием, бывают две проблемы: - непринятия его целей и методов; - непонимание того, что есть доказательность.
Говоря простыми словами, доказательность, в любой сфере, - это представление рассматриваемого явления в такой форме, что утверждения относительно него (например, о его правильности) становятся очевидными, для любого человека, но при условии определённой (зависящей от применённого представления) теоретической/методической подготовки.

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

С точки зрения целей инженера, всякий метод, который позволяет делать очевидной правильность какого-то класса создаваемых конструкций, есть большой шаг вперёд. Если этот метод уменьшает трудоёмкость по сравнению с каким-то более общим/мощным - это тоже шаг вперёд. Иногда трудоёмкость для простых задач снижается настолько, что исключается необходимость применения полного мат. аппарата.
Примером являются базовые схемы циклов.

(ветка закрыта для обсуждения как флеймоопасная, желающие дискутировать могут завести свою ветку во Флейме или в Опять-25. Важное и по делу перенесём сюда).