I've been working on a guaranteed-terminating language in the vein of APL/J. Primitive recursion is possible, but with the looping all implicit due to array shape, infinite looping is impossible. The issue I'm not sure how to handle is that some algorithms take the form, "repeat the following until convergence: ..." with no obvious way for a machine to prove that convergence will eventually happen.