[dllthomas]

"(an evaluator for programs in an at-least-as-powerful dependently typed language is the only remotely natural example I know of)"

Note, also, that there's an obvious restriction for that case to get something you can write: "evaluate for the next X steps".