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

Очень интересный жизненный цикл получения этого кода (сам код на C, но прототип на Haskell. У меня складывается, что написание сразу двух эквивалентных программ на двух разных языках является сейчас магистральным направлением для хорошо верифицированных и надежных программ -- тот же Harold Lawson употребил этот прием для архитектуры Cy-Clone, коды которой писал на ассемблере, а исполнимые комментарии на чем-то типа Паскаля, а затем добивался одинакового исполнения кодов и комментариев -- "для проверки" Для верифицированных даже поболее двух :). Целевой язык, язык спецификации, язык для автоматизации доказательств. В идеале, реализацию можно извлечь из конструктивного доказательства корректности спецификации.