I think "declarative" exists on a spectrum. There's no clearly defined line between declarative and nondeclarative that I know of. For instance I would say Haskell < Prolog < SQL are on one end of the declarative spectrum, but in each case you do end up reasoning about the underlying execution model.
This is a fair statement. What I (and I believe most others) mean by declarative programming is more specifically logic-and-constraint programming, but in many ways you could view Haskell's type system, typeclasses, and laziness in combination as being more declarative than, say, a purely functional subset of Scheme. To the grandparent post I originally responded to - If you wanted to take a look at a more purely declarative language, see miniKanren
https://docs.racket-lang.org/minikanren/index.html
There exists an extension with constraints as well, cKanren
http://scheme2011.ucombinator.org/slides/Alvis2011.pdf
To try to summarize, a declarative language is one in which you tell the computer what you want, but not so much how it is done. Logic Variables (Unification) are the key differentiators of these systems.
Take a look at chapter one of CTM for a really nice breakdown of the different orthogonal components to a language. I have a feeling differentiable programming and (dependent+) types belong on that list, too.
As an additional question of my own for anyone reading - is there anything that should be on that list thanks to modern CS research, that isn't?
