Page 163 of the book Software Abstractions has this remarkable statement:
The declarative style of description is very powerful, but it has a downside: inadvertent overconstraint.
Wow!
Is "inadvertent overconstraint" a problem that occurs in all declarative languages? For example, does inadvertent overconstraint occur in XML Schema? Does inadvertent overconstraint occur in SQL?
In other words, is the "inadvertent overconstraint" problem peculiar to Alloy, or is it widespread and applicable to all declarative languages? If it's the latter, I would be most grateful for an explanation.
It's the flipside of the benefit that conjunction brings. In a programming language, you can't write a sort by saying "the output is a permutation of the input and the elements are in order", but you can say that in a specification language that allows and. This gives a lot of power, especially by enabling separation of concerns, and it lets you start with minimal constraints and then grow them. But there is a downside: add too many constraints, and you might end up at false (or worse, something just a bit stronger than you intended). Alloy's unsat core facility is helpful at dealing with this, but doesn't solve the problem entirely.