> 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?"

> Even if its an engineer that's making 6 figures that you are liekly alluding to, do you expect everyone to agree with your moral code and quit their job?

No, but you shouldn't expect to see them addressed with respect either, just like Enron traders, Purdue salesmen or tobacco scientists don't get a lot of it.

Stuff available on the internet is also the result of a lot of research, time, money, and expertise. And AI companies taught us that it’s OK to yoink whatever is not bolted to the ground, even when it is illegal to do so.

I now picture people talking to their washing machine like the intro of american psycho.

I have seen smiling people talking to their connected car, replying with a dumb condescending bad-actor voice.

I had also seen Frankie Boyle in his parody of Knight Rider: "Michael, I am Kitt, your car, stop taking the medications, they want you to take them so you will be unable to talk to me"...

That is outlook.

There is no reason to have an os or a language dedicated to such specialized tasks.

Yes there is, at least to me. The reason being total freedom to tune the operating system, and not being limited to what someone imagined I would want to do in the future.

No cardboard, no cardboard derivatives, no cellotape.

> to compete with major carriers worldwide.

I don't see a reason why countries with existing carriers would allow that, given the owner's stance about political meddling.

They would be as large as your average hyperloop capsule.

> The problem is, global warming doesn't affect daylight.

In my book, that would have been a "Fortunately," entry.