Two examples that satisfy these criteria are Dhall [1] and Cue [2], but in one sense they are not interesting examples: Dhall is a total language on purpose, it does go the “not Turing-complete” route, and Cue has no functions so there is nothing to recurse.

I would say that RCL [3] satisfies the criteria. It’s deterministic and pure, has metered execution, and it sandboxes filesystem access. It can read files when allowed by the sandbox policy, but in my view that makes those files part of the source code, it behaves the same as imports.

For RCL I did not want to go the “not Turing-complete” route for exactly the reason the author mentions: knowing that a program enventually terminates is not a useful property in practice. And conversely, it is possible to write very complex programs in total languages like Agda, non-Turing-completeness is no guarantee for simple programs/configurations. All loops in RCL are bounded, but it has functions, so it has recursion. It does not have tail calls, so at first I added a recursion depth limit (to prevent overflowing the native stack), but then the fuzzer discovered a function that runs in constant stack space, yet it hangs. I still don't fully understand how it works:

    let f = g => g(g(h => k => g(g(h))));
    f(f)

Anyway, it is not a problem in practice that this kind of pathological function can be expressed, I just put a limit on the number of execution steps (a “gas limit”, or what the author calls “metered execution”). For keeping code simple, I think the fact that the built-in looping constructs are bounded, and recursion is awkward, are a good nudge, but in the end the most valuable tool is code review and applying good judgment.

    [1]: https://dhall-lang.org/
    [2]: https://cuelang.org/
    [3]: https://rcl-lang.org/