@Dmitry Oh, thanks; I'd say that's similar enough to close my question as a duplicate. Briefly looking through the responses, it seems like the answer is "we're not sure yet; we're working on it."

Formality is a (kinda) procedural language that forbids infinite loops (when you use the type checker). Last I checked, you satisfied the requirement by either specifying a max recursion depth, or by providing a proof that your code does indeed terminate. It's still a pretty beta-stage language, still in flux I think, but it has some nifty ideas, and (last I checked) it's quite operational.