Interestingly, Coq is expressive enough to write arbitrary computations; for example, you can write a Universal Turing Machine emulator; or, more realistically,

Interestingly, Coq is expressive enough to write arbitrary computations; for example, you can write a Universal Turing Machine emulator; or, more realistically, many people write programming language implementations in Coq, in order to prove results about them. However, Coq can only run those computations for a given number of steps; in other words, you can't say "run this until it halts, and give me the result", but you can say "give me the result after 3^^^3 steps, or 'Nothing' if it hasn't halted by then". The reason this is interesting in this discussion is that Ethereum uses "gas" in a similar way.