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)

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

I don't think it actually runs in constant stack space, but it takes an exponential number of execution steps to get to any given stack depth, as the number of function arguments that need to be unraveled doubles with every invocation of f.

CUE developer here. This is wrong. CUE doesn't have functions, but it does have abstraction and beta-reduction, just like lambda calculus. Types can refer to themselves. There is also mutual recursion between types. We have a termination checker than ensures CUE programs are total (although it works by very different principles compared to other total languages).

If you disable the CUE termination checker you get a a Turing complete language.

If you leave it alone you get a primitive recursive language. Here is CUE implementing an arbitrary number of steps of rule 110 cellular automaton[1], which is Turing complete: https://cuelang.org/play/?id=Ityqia88Mvq#w=function&i=cue&f=...

[0] https://en.wikipedia.org/wiki/Rule_110

Dennis Ritchie's research at MIT was focused on what he called loop programming.

The complexity of loop programs - ALBERT R. MEYER and DENNIS M. RITCHIE

https://people.csail.mit.edu/meyer/meyer-ritchie.pdf

Structured programming, the paradigm that almost every modern programmer follows by default is really pushing you to primitive recursive functions.

That almost universal acceptance of structured programming compared to the other two types, pop and functional, is why people are confused about Dykstra's goto is harmful paper.

While primitive recursive functions don't contain the entire set of computable functions, they do contain almost all intuitive ones that are guaranteed to HALT (total).

Unfortunately there are some real needs for languages to support loops that have an indeterminate number of iterations when you enter the loop, but it is a foot gun that is avoidable by only using them when required.

Even COBOL was modernized with unrestricted goto being moved to the ALTER command.

I can't think of a modern, useful language that doesn't allow for PR functions.

But even in C, if you avoid 'while', explicitly avoid fall through, etc... you will produce code that almost always is a total functions that will always HALT.

There are cases like even type inference in ML, which is pathological in that it is way cheaper than the complexity class, thus worth the risk, despite not being total functions that make it hard for a language to restrict those use cases.

So I would say that with a pragmatic approach, all languages support defaults that support most of the points, but imposed constraints that enforce them would seriously constrain the utility of the language.

If you review even the hated SOLID and Clean frameworks, they're pushing you towards this model too IMHO.

I think the universal acceptance of structured programming, makes this easy to forget or even fail to teach. But as an old neck beard, we were taught the risks of WHILE etc...

Isn’t the advantage that an upper bound on the number of steps required can be computed statically?

This means we can refuse to compute things that violate some limit and give back a meaningful error, for all possible inputs.

Whereas with the Turing complete plus Runtime Limit approach, we might pick a limit that is too low for some inputs we care about. We won’t know until we run the computation and hit the limit! We see this sometimes with C++ template recursion.

I might be totally confused here so I hope some more knowledgable can weigh in :)

But I usually run into this problem when someone has treated the problem domain as a DAG but can’t enforce the Acyclic part. But modeling your problem as a DAG is reminiscent of Dark Galadriel, when she contemplates taking the arming from Frodo - All Shall Love Me and Despair. The people who make them are always way prouder of themselves than they deserve to be.

Eventually your customers who were attracted by the expensive and complex solution to their problems run out of money, and their problems seem a lot smaller to them. Then you are left - literally - with an app that cannot be made cheap enough per operation to keep their business.

I'd be more interested in using it just as another hammer in the tool-belt to squash bugs that got past earlier hammers (static type-checking, no nulls, no mutations, etc.)

Terminating in finite time can't prove correctness, but if I declare that my code will terminate in finite time and my compiler disagrees, I'd certainly believe my code is incorrect.

Note: This assumes lazy evaluation, or short-circuiting conditionals, in order for early exits to affect the runtime, but that’s what you’d generally have in a practical language.

But I struggle to think of a single situation in which that's a real hard requirement. How many systems are there that can't give a "query took too long" error?

> If math makes you slightly nauseas

That's the plural of nausea, you wanted nauseous.

But the real reason I mention it is to joke, since you said you were generally descriptivist, that you fell for a common error and actually 'nauseous' describes the thing that makes someone nauseated. ;)

> Typically, not being Turing-complete is extolled as a virtue or even a requirement in specific domains. I claim that most such discussions are misinformed — that not being Turing complete doesn’t actually mean what folks want it to mean

Why are those discussion misinformed? Most formal analysis tools (Coq, Isabelle, Agda(?)) usually require a proof that a function terminates. This is I think is equivalent to proving that it is total implying it is primitive recursive?

Proving a function is total in the general case is a NP total search problem.

IIRC this is equivalent to NP with a co-NP oracle, or the second level on the PH hierarchy, aka expensive if even possible even in many small problems.

Most of those tools work best if you structure your programs to be total, of which structural programing with only FOR or iteration count limited WHILE/recursion are some the most common methods.

While just related to SAT, look at the tractable forms of Schaefer's dichotomy theorem is the most accessible lens I can think of.

My intuition suggests this should be undecidable—could you elaborate on the difference between this and the halting problem?

The HALT decider is a total Turing machine that represents a total function.

I am struggling to explain this in a rigorous fashion, and there are many open problems.

NP is where the answer "yes" is verifiable in polynomial time.

co-NP is where the answer "no" is verifiable in polynomial time.

NP is equivalent to second order predicts logic where the second term is existential 'there exists..'

co-NP is equivalent to second order predicts logic where the second term is universal 'for any'

We know P=co-P, or that the yes and no answers are both truthy.

We think that NP!=co-NP

Many useful problems are semi-decidable or recursively enumerable.

Determining if a computable function is total is not semi-decidable.

It is the subtle difference between proving a TM halts for any input vs halts for each input.

Termination analysis is the field of trying to figure out if it halts for each input. It is actually harder than HALT, being on the second level of PH on the co-NP side.

If that granularity isn't important to you, I personally don't think there is much of a risk in using the decidable metric as a lens.

Just remember that something is decidable if and only if both it and its complement are semi-decidable.

Semi-decidable problems often have practical applications even without resorting to approximations etc ...

You claimed in GGP that deciding whether a function is total is a TFNP problem. In particular, that would make it decidable. But the counter-claim is that deciding whether a function is total is actually an undecidable problem.

I've also examined a definition of TFNP and I don't see how it is related to the problem of deciding if a function is total. Rather, the definition seems to require that the function in question be total.

The halting problem only asks: given a TM and input, will the TM halt on that input? That problem is actually semi-decidable/provable: we just run the machine. If the answer is yes, then at some point it will halt!

No, as the article shows there are functions which terminate that aren't primitive recursive, and indeed Agda and (probably?) the others can prove termination for some (but necessarily not all) terminating non-primitive-recursive functions.

I think the misinformation that the article is complaining about is something like (my paraphrase):

> "Turing completeness" means "can do computation" while "non-Turing complete" means both "can't do computation" and "has nice configuration-language properties"

The article points out:

- you can be non-Turing complete and still do lots of computationally-expensive / tricky work

- your configuration language probably wants much stricter limits than merely being non-Turing complete

> > "Turing completeness" means "can do computation" while "non-Turing complete" means both "can't do computation" and "has nice configuration-language properties"

"Turing complete" means it can do any computation a Turing machine can. That is absolutely more power than is desired about 99.99% of the time. You almost always want your algorithms to contain no infinite loops.

(Algorithms. Not IO loops. Those are different, and the process of taking outside input while the program is running is outside the scope of what a Turing machine talks about anyway.)

Turing completeness is an ergonomics hack, and one with a decently successful history. But it's no panacea, and if we could find an ergonomic way to get rid of it, that would be a win.

Yes, even if we didn't also enforce primitive recursion. Sure, it's nice to know you're also not accidentally running Ackerman's function, but to be honest... I've had many more accidental infinite loops than accidental Ackerman's functions in my code. By approximately 10,000 to 0.

No system can ever prevent all errors. So let's focus on preventing the most common current ones.

Mistakes like "your" instead of "you're" and "should of" instead of "should have" seem to be very common for people who learned english by listening instead of reding (native speakers). The words sound the same, so they get switched.

On the other hand, as a non-native, I struggle with phrasal verbs, such as "get in" vs "get on", "get out" vs "get off", and so on. These may be very different concepts in English, but not for my native language, so I don't always choose the correct one.

I agree with the author with regards to the stronger semantics, and that's why I thought of this language. You often want to have some guarantees over the execution time of your program. It would probably be PRF based at the core, but Turing complete in practice. Like how rust rejects invalid borrows but still offers unsafe for raw pointers, this lang would either calculate the upper bound based on the simple loop primitives, or you'd have to use the unsafe operators and provide an alternative formula for the bounds.