> -- Geniepro писал(а):
> Не будет ли столь любезен многоуважаемый джин, что поведает нам об этих более коротких и надёжных путях, которые не являлись бы лишь частью того пути, который прошли эти австралийцы?
Уважаемый Джин-Про не хуже меня знает, что нисходящее проектирование в сочетании с формулировкой логических предикатов и с опорой на строгий язык обеспечит не меньшую надёжность. Время, потраченное на переформализованную рутину, лучше потратить на хороший дизайн и проверку системы несколькими людьми.

Потому что тех, кто понимает суть формальных методов, сама по себе мантра "мы формально доказали..." не убеждает.

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

Как будто что-то заоблачно трудное - написать безотказное ядро.

Суть обсуждаемых работ - возможность применения Хаскелла с некоторым формальным аппаратом для надёжного программирования. Т.е. исследование новых для Хаскелла вопросов. Но не новых вопросов для надёжного программирования.