brainfuck interpreter in Coq - まめめもHaskell 、Erlang の次のブームは Coq に違いありません。とりあえず基本ということで、Coq でひねりのない brainfuck インタプリタを書いてみました。動作例。Coq のコードが色づけできないとは何事か。 Eval compute in (finite_execute " +++++++++[>++++++++>+++++++++++>+++++<<< -]>.>++.+++++++..+++.>-.------------.<++ ++++++.--------.+++.------.--------.>+. " "" 500). = "Hello, world!"%string : string 残念ながら (?) Coq では停止性が保障された関数しか定義できません。ここでは最大評価ステップを指定しないといけないという仕様にしてごまかしています (引数の 50
