> E.g., I've seen some people brag about some configuration language being easy to mechanically analyse because it's not Turing-complete, while in fact it's at least PSPACE-hard to analyse.
I don't get your point here. What analysis are you talking about?
I believe the claim usually made about non-turing-complete languages is that it is possible to prove specific properties with little to no calculations, that would be otherwise hard to calculate. For instance, the time needed to determine that an Idris program will eventually stop is litteraly 0 seconds.
> I don't get your point here. What analysis are you talking about?
Determining any kind of non-trivial property (i.e. a property that isn't true for all or none of the programs in the language).
> I believe the claim usually made about non-turing-complete languages is that it is possible to prove specific properties with little to no calculations, that would be otherwise hard to calculate. For instance, the time needed to determine that an Idris program will eventually stop is litteraly 0 seconds.
It's not the non-Turing-completeness that makes that practical. Let's take your example of Idris:
1. If a program's termination is hard to determine, then it will be hard to write it in Idris. I.e., the effort isn't gone, it's just shifted elsewhere. And if the program is easy to write in Idris, then its termination is also easy to prove in other languages (Idris effectively requires you to write a proof of termination, but you can write the proof for any language).
2. The importance of this is not as high as you think. For example, we can trivially rewrite all of the world's software in an always-terminating language (so not-Turing-complete), by changing the semantics of all programs to terminate after 2^100 steps. This will not affect the behaviour of any software, and you can see why it also won't make determining any of their properties of interest any easier.
So yes, Idris makes termination a trivial property for Idris programs, but it doesn't make the effort of determining whether an algorithm terminates or not easier (you just have to do it _while_ you're writing the program instead of after), and it doesn't, by itself, make any other property (which remains non-trivial) easier, such as "does the program terminate in fewer than 2^100 steps?"
> Idris effectively requires you to write a proof of termination, but you can write the proof for any language
That is the benefit of non-turing complete languages, though. Or, in general, the point of languages with useful type systems.
Writing the proof is not trivial, but languages like Rust or Idris make it simple because they force correctness early in the coding process.
> That is the benefit of non-turing complete languages, though.
That's simply untrue. You can write arbitrary proofs about programs in Turing-complete languages, too. In fact, most formal proofs are of programs written in Turing-complete languages.
> but languages like Rust or Idris make it simple because they force correctness early in the coding process.
Rust doesn't actually let you do that, though. In terms of the expressive power of proof, it is far closer to C than to Idris (in fact, from Idris's vantage point, Rust is almost indistinguishable from C).