Prolog is Turing-complete, and Datalog isn't. In light of this, I think it's a bit of a stretch to call it a (logic) programming language. But people seem to do that.
Turing completeness is a bug, not a feature. After writing code in Agda for some years I was convinced that Turing completeness does more harm than good. Non-TC languages have a killer feature: their halting problem is solvable which means you can get arbitrarily strong guarantees from the compiler. The fact that you can't encode "while(true) { }" without putting "unsafe" doesn't make the language impractical, you can still implement algorithms without Turing completeness.
Moreover, using various forms of coinduction you can encode infinite computation even in non-TC languages.
Agda's been around for 24 years, according to Wikipedia, and it hasn't exactly revolutionized software development: I'm not aware of any notable software written in it, or of anyone so much as winning a programming competition while using it (and some of those are designed to promote functional programming) So, frankly, I'm skeptical that Agda's trade-offs in the performance-convenience-correctness space are good.
Ok, ok I understand theoretically what this means in terms of programming languages. But what does it mean practically? What features are removed? How does this work out when you're implementing a program?
Turing completeness is not a requirement of a programming language! Just because you can't do infinite computation doesn't mean you can't do infinitely useful computation :)
That said, Souffle is touring complete due to its adding of constructors to the language.
