Yeah they have the rights to do it, doesn’t mean it’s a good thing to do, doesn’t mean it won’t negatively impact the future of the project.

Redis had the rights to change the license of redis, look at where that led them.

I did say “general purpose”. And many proof assistants are Turing Complete actually, such as Lean.

It’s not what you can use that language to do - all general purpose languages are Turing Complete, so what you can do with them is exactly equal. It is about what the language will do for you. Rust compiler will stop you from writing memory unsafe code, C compiler cannot do that.