> -- Geniepro писал(а):
> История этого микроядра забавная -- сначала эти австралийцы сделали микроядро на Хаскелле, верифицировали, конвертировали вручную на Си, и вот, наконец, доказали, что их микроядро seL4 соответствует первоначальным исходникам на Хаскелле...

Не трогая сам по себе Хаскелл...
Занятный пример якобы математики без понимания этой самой математики...
Мартышкин труд доказательства неизвестно чего неизвестно зачем.
Типа, волшебные формальные выкладки что-то там гарантируют.

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