Not sure why you're being downvoted. This is the problem. Whenever you want any guarantees about anything you implement a very restricted[1] subset of what a T

Not sure why you're being downvoted. This is the problem. Whenever you want any guarantees about anything you implement a very restricted[1] subset of what a TM can do... at least if you're allowing users to input arbirtrary programs[2]. If you don't restrict to a non-TC language... you're -- in so many words -- fucked. (Hence the "hack".) [1] Preferably using a statically typed PL, for obvious reasons. There's actually a thing these days where non-TC languages can actually "do things". My favorite moniker for this is "pacman-complete" (coined by Edwin Brady, I believe.) [2] Having looked at a few .sol files earlier, they at least look TC, having general recursion and all.