Declarative approach
A style of writing where a program is a system of rules and constraints describing the desired result, with no order of steps: it states what must hold, and an engine decides how to get there. Database constraints and queries, inference rules and descriptions of a system’s desired state work this way. Example: “bookings of one room never overlap” and “a booking lasts at most 4 hours” as database constraints. Simple declarative notations can be checked exactly from the text, because their behaviour is visible in the statement itself. In a powerful declarative language this no longer holds, and Rice’s theorem hits it just like imperative code.
Where it shows up: languages, validators, engines
- SQL · a query says which data is needed and the database picks how to fetch it. CHECK, UNIQUE and EXCLUDE constraints are rules the database enforces on every write.
- Kubernetes · you describe the desired state: which services and how many copies to run. Controllers in a reconcile loop bring the system to it.
- JSON Schema · a schema describes the shape of data; a validator checks every document against it.
- Quint · as well as TLA+ and Alloy: system rules and invariants are written as statements, and model checking goes through the states.
- Z3 · constraints on values; the solver finds values that satisfy them or proves there are none.
- Prolog · facts and inference rules; the engine finds the answer to a question itself. The language is complete: an endless loop can be written in it too.
- Datalog · a cut-down Prolog for querying data: every query is guaranteed to finish, so the answer is always exact.
Source: Wikipedia: Declarative programming
Read more: Where to check an AI agent's workA reconcile loop for specs: like KubernetesHow model checking differs from testingSpecs by aggregate
Where it appears · 2
- Where to check an AI agent's work · Specs and context
- Rice's theorem in plain words · Specs and context