Re: Declarative constraints in practical terms

dawn wrote:
> ralphbecket_at_gmail.com wrote:
> > Specifications should be (and usually are) given in a declarative
> > language (e.g., first order logic) which can only state *what* the
> > invariant is, not *how* it should be computed or maintained.
>
> I understand that people state this as if it were obvious that a) we
> must specify what not how and b) we must constrain ourselves to 1st
> order predicate logic and c) having a mathematically simpler
> sublanguage to work with makes for better quality code. I do see
> something elegant about being able to call a proposition p and a
> constraint q and then ask p ^ q? But we can do that in a general
> purpose language too, right? We don't have to use the full
> expressiveness of the language (if there is some reason not to) nor
> does using a functional language (or other) make it harder to code the
> average constraint, I would think.

Here's the difference: if your specification is imperative (i.e., it says how
something should be done, but nothing about the meaning of the constraint), then an implementation must follow that prescription *exactly*.
There is no room for manoeuvre. Also, there is no meaningful way of deciding when two constraints are inconsistent, because they are both specified purely in terms of changing one pile of data into another.

If your specification is declarative (i.e., it only says what should be done),
then any implementation that meets the specifcation is sufficient.

For example, say my declarative specification is "n must be a prime number". I can write this formally as

prime(n) <=> |{x | x is a factor of n}| = 2

I have complete freedom in my choice of implementation (e.g., I could do a naive search for factors, or I could use Eratosthenes sieve, or I might use a suitably robust statistical primality test, or anything else
that did the job).

An imperative specification of the constraint would have to pick just one
of those possible implementations and say "this is exactly how it will be done", but not say what the point of the procedure is.

> > If the specification is implemented in an adequately expressive
> > declarative implementation language (such as that provided by
> > the DBMS), at most all one needs to do is make slight changes to
> > the syntax in the spec. to convert the specification to the
> > implementation language.
>
> Similarly in whatever language, I would think.

Sure, from a sufficient distance all these things are equivalent. But it
would be pointless to write a Java application to solve a problem that could more easily be handled by a spreadsheet. The two languages are completely different and the amount of work required to code up and verify a particular problem in a spreadsheet is vastly less than that required to do it in a Java program.

> OK, I think I'm following you here. As long as we use a sublanguage
> that is sufficiently restrictive rather than using a general purpose
> language, we can execute formal proofs that the implementation meets
> the specification (provided the specification is written in some way?)

Declarative languages can be perfectly good general purpose languages (cf. Mercury).

This is not about restricting expressive power, it's about increasing it!
Imperative languages force you to express yourself at such a low level that it takes much more work to show that an implementation meets a specification.

> The reason we restrict ourselves with a sublanguage instead of using a
> full-featured language is somehow related to the provability of the
> code.

It's not a sub-language.

It's not only about the provability. It's about the level of abstraction,
the ease of maintenance, and the vastly increased opportunities for optimisation and automatic checking.

> Is there a clearly established correlation between this type of
> provability and quality?

What sort of evidence would convince you? I, too, would like to see evidence for the counter-argument to support your position that imperative languages are a sensible choice.

> If so, why do we ever use a general purpose
> language? Even if it is required for some things, why do we use a
> general purpose language for so much that doesn't require it?

Because it's what most people are taught. Languages like Java and C# and movements such as OO and XML etc. have all had fantastic marketing machines behind them which have simply stated without proof that each has been the best thing since sliced bread. People in the computing business suck up this stuff with an alarming lack of scepticism.

> > This sounds like you're thinking imperatively (IO is necessarily
> > an imperative concept). IMHO it's better to think in terms like
> > "this table must maintain a one-to-one mapping from keys to
> > values" or "the values in this column of the table must form a
> > contiguous set" or "all keys in this table must be members of
> > the Employees set".
>
> Why do you think this is a better way to think? I know a lot of people
> think this, but I don't see that as obvious at all.

Imperative specification: "Bring cream to a boil, and boil about 30 seconds.
Pour it immediately into the egg yolks and whisk them together. Return the
mixture to the pan and continue cooking without allowing it to boil. Stir the
mixture until it thickens and coats the spoon. Pour the mixture into a

shallow baking dish. Refrigerate overnight. Two hours before the meal,
sprinkle the chilled cream with the sugar in an even layer..." and so on and
so on...

Read that and then tell me that you instantly cottoned on to the declarative specifcation: "cook a creme brulee".

> > > Do coders who write constraints
> > > declaratively code more accurately and more quickly?
> >
> > Yes, in my experience - but then I am a Mercury developer.
> > Plug: www.mercury.cs.mu.oz.au
>
> OK, so you really like this way of coding. Is there proof this is
> better or is it a matter of taste and different brains working
> differently?

What do you want as proof? There are any number of articles on the web about the benefits of declarative programming, but I'm not sure that constitutes proof. What is the "proof" for prefering imperative languages instead?

> > This is just one data point, but it is quite a spectacular data point.
>
> I've got my anecdotes too in other areas, and I'll accept yours as
> potentially indicative.

I'm curious: give me an anecdote where the declarative approach was demonstrably inferior to the imperative approach.

> > As I said above, converting a declarative spec.
>
> what if my spec is imperative?

Can you give me an example? As I've tried to show in two examples above, an imperative spec. is not really a spec. in any useful sense.

> > into a declarative
> > implementation language is usually very easy to get right: there is
> > often a simple correspondence between the spec. language and
> > the declarative implementation language.
>
> and a simple correspondence between an imperative spec and an
> imperative language?

If you really believe that imperative specs. have value.

> > With an imperative language like Java I have to write a program and
> > then prove that the result of executing that program (which is written
> > in terms of *how* computation should proceed, not *what* is being
> > computed) meets the spec. Nobody does the last step
>
> and they do with SQL constraints?

SQL constraints are declarative. You couldn't implement an imperative spec. in SQL because SQL has no concept of "instruction". SQL constraints already say exactly what they mean, just not how the DBMS should enforce them.

> > Do you really find it plausible that human coders could do better than
> > an automatic optimiser on a day to day basis? Especially where these
> > coders are already struggling with concurrency and distribution and
> > don't have access to internal DB structures?
>
> I can imagine that much can be automated and packaged in reuable
> libraries. I'm not suggesting that we want to write custom code for
> anything more than what is coded in constraints in a declarative
> language, but I am suggesting that the language could be any.

I don't understand what packaging functionality in a library has to do with
automatic optimisation in a live DBMS.

> > But there is an industry standard language for this which everybody has
> > to use at some point: SQL!
>
> I don't have to. I do, but I don't have to. I know a lot of folks who
> write data-based software and don't use software.

Sorry, I'm having real trouble understanding those sentences!

> You can find some of
> them at comp.databases.pick. Soon you will find others that work with
> xml data sources.

What does this have to do with expressing constraints declaratively?

> > > > If you like, (a) has fewer moving parts.
> > >
> > > It seems to me that it has the same number, but fewer that are not
> > > delivered, tested, etc by the DBMS provider.
> >
> > No, no, no! (a) has fewer moving parts (zero, in fact) because it
> > never
> > says anything about *how* things should be done.
>
> "It" (that being the entire software solution) includes the constraint
> engine, which surely has moving parts.

You can throw in the compiler and the OS and the kitchen sink too, but that is not what we are discussing. We are discussing properties of the languages used to enforce constraints.

> Given this "selling point" of yours, you might find this somewhat
> amusing
> http://www.tincat-group.com/mewsings/2006/01/data-movement.html

Hmm. I don't buy it!

• Ralph