Many years ago Ed Ashcroft and I invented the declarative language Lucid. It’s had an
interesting history.

To begin with, we never intended to design a dataflow language. All we wanted was
a more rigorously structured language which would make it easier to prove assertions
about programs.

I’d moved into computer science after leaving Berkeley and soon became convinced
that this new-fangled “structured programming” was the way to go. In fact I quickly became a real fanatic, convinced that not only did the goto statement have to go, but that even assignment statements caused trouble. My objection to assignments was that they looked like equations but were typically used in a way that defied the logic of equality. For example, early in a program you can have

I = 1

but later you can have

I = J*J+3

which contradicts the first equation. Even worse, you can have

I = I+1

which contradicts itself (because it implies 0=1). No wonder program proving is difficult!

Actually, my objection was to re-assignment, and I began trying to find a way to program without reassignment – with only one assignment per variable. The problem, of course, is loops. For example, writing a loop that makes I a counter, starting at 0, seems to require two (contradictory) equations, I=0 and I=I+1. It occurred to me that the apparent contradiction could be removed by making it clear that the first equation is true at the beginning of the loop, and the second is true on each subsequent step. My scheme was to use keywords “first” and “next” as follows:

first I = 0
next I = I + 1

After a few days of looking at these equations I realized they could be parsed differently –
as

first(I) = 0
next(I) = I+1

These mysterious functions first and next looked really promising; the following equational laws seemed obviously true:

first(I+J) = first(I) + first(J)
next(I+J) = next(I) + next(J)
next(8) = 8

and so on. Also, the loop induction rule could be formulated very simply as

first(P), P -> next(P)
———————-
P

I was convinced I was on to something and ran to see my friend and colleague Ed Ashcroft (we were both at Waterloo at the time). I was amazed by his reaction, which was basically, fascinating, but what is the semantics? I waved my hands rapidly and said “first(I) is the first value of I, next(I) is the next value of I”. He wanted something more precise but I had nothing to offer. Back in my office, I could see the problem. Since next(0)=0, next(1)=1, next(2)=2, and so on, it ought to follow from the rules of logic that next(I) is always I (assuming we are computing with only the natural numbers). But next(I)=I+1 is supposedly consistent. Not as simple as it appears … (to be continued)