Там использован старый принцип: программа на ivory представляет собой код на haskell, результатом выполнения которого является код на С. Ну а типовой контроль держится на системе типов haskell:
fib_loop :: Def ('[Ix 1000] :-> Uint32) fib_loop = proc "fib_loop" $ \ n -> body $ do a <- local (ival 0) b <- local (ival 1) n `times` \ _ -> do a' <- deref a b' <- deref b store a b' store b (a' + b') result <- deref a ret resultОбращу внимани на тип параметра - "от 0 до 1000" - то есть это не совсем фиббоначи (на Ivory кажется non-terminated программа вообще невозможна - но как ни смешно - писать на этом можно - они вон цельный автопилот для квадрокоптера написали)
Сам по себе прием очень старый - помнится еще у Терехова "Самсон" микропрограммировали посредством комплекта операций и функций на А-68 результатом исполнения которых был собственно микрокод. Коля Ф. с Тереховым как-то срался "на чем микропрограммируют самсон" - Терехову было надо естественно в целях пиара чтобы "на А-68" хотя на деле конечно нет.
Потом еще Tcl как макроассемблер пользовали (ну в смысле команды просто описываются как tcl-процедуры и вперед) etc
Ну в общем приятно видеть что прием не забыт.