> -- Alexey Veselovsky писал(а):
> Вообще, такое ощущение что они доказали правильность работы транслятора haskell->c для данного конкретного исходника.
Данный конкретный исходник транслировали люди, вот их работа и проверялась программой доказательства теорем.

Почитайте статью "Running the Manual", там описан их подход -- итеративный дизайн спецификации и реализации микроядра и его API, построение модели ядра на Хаскелле, выполнение его с некими прикладными программами на эмуляторе процессора, конвертирование хаскельного кода во входной язык системы доказательства теорем Isabelle с проверкой его свойств...