interesting article from HN today - http://neilmitchell.blogspot.com/2020/11/turing-incomplete-languages.html

I think cedille is on to something here. https://arxiv.org/pdf/1903.08233.pdf I may be wrong here, but because of the basis of equality on beta-equivalence, you get some nice properties of writing programs with general recursion

The author seems to consider a rather specific sub-species of Turing-incomplete languages: those that try to be as close as possible to Turing-complete except for preventing non-termination. I haven't looked at any of those. What I am much more interested in is languages that reduce computational abilities in return for better reasoning about data and code. Something in between HTML and JavaScript, for example. Has anyone seen work on such languages?

@Konrad Hinsen Dhall leverages non-TC for safety guarantees: http://www.haskellforall.com/2020/01/why-dhall-advertises-absence-of-turing.html

Dhall is a cool use case for strong normalizing since most people feel uncomfortable with powerful languages for configuration

@Prathyush Dhall looks interesting indeed, thanks for the pointer!

@Konrad Hinsen I worked with elm for a while. While it has general recursion, the elm architecture really limits what you can do with it. The only functions you can write that ever get executed by the runtime have pure signatures. Now I really hate elm

Oh yeah, that makes me think that Datalog also has terminating guarantees because of lack of negation(?). So does SQL if one takes out recursion.

Just wondering: why is everyone focusing so much on termination? In my personal debugging experience, endless loops are a rare issue and usually found and fixed quickly. As long as the OS allows interrupting a process... what's the problem?

When you phrase it that way, robustness seems to be the opposite of expressiveness

Yes and no. It's the opposite of expressiveness if you think about general-purpose programming. But I am thinking of DSLs. If your robustness criteria are those of the domain you design for, they don't imply a loss of expressiveness.

Yeah I don’t think termination is really so interesting. I think there’s a good metaphor out there but I can’t bring one to mind. I do like what you get with more expressive types though. Those usually require totality

I came to the same conclusion, that requiring provable termination isn't useful, but perhaps it's a useful default - perhaps a language can be designed such that it can prove most programs will terminate, and for cases where it can't prove it, you'll get a warning that you can then turn off (either by 'conjecturing' that it terminates, or declaring that it doesn't always terminate and the programmer just accepts it). However, if I was building a language, there are other type-system features I would prioritize over termination analysis (e.g. unit inference).