Без заголовка

написание сразу двух эквивалентных программ И даже не обязательно программ. Можно дополнить программу неисполнимыми спецификациями (например, пред- и постусловиями) и получить аналогичный результат. Даже лучше, чтобы использовались различные парадигмы - процедурный и функциональный языки, язык программирования и неисполнимые спецификации. В одной парадигме проще делать одинаковые ошибки. добивался одинакового исполнения кодов и комментариев На всякий случай - тестирование не доказывает эквивалентности. Надо еще почитать, а как они доказали, что в Haskell прототипе нет багов :)