Why Alloy has no in-built Notion of State

A few years ago Daniel Jackson took the rather surprising step of actually removing in-built support for states from the Alloy specification language. Here he explains why:

the main advantage of the old scheme was that, with the notion of pre and post built in, certain mutability constraints could be built in too. when you declared a state component, you could say how it changed.

but it turns out that priming as an operator is much more complicated than you would imagine. it made for all kinds of kludges in the implementation, which was a sure sign that the semantics was too complicated. and sure enough, if you take a look at the semantics of sequential composition in the Z standard, you'll see that it's full of subtle details and is really quite ad hoc.

the main reason we dropped it, tho, was that we wanted to be able to handle dynamic behaviour with more flexible idioms. with that priming convention, you're really tied to a rather narrow way of writing models. having got rid of it, we can do more ambitious things -- talking about sequences of more than a pair of states, for example.

(From the alloy-discuss group.)

One of the reasons that I became disillusioned with Z and its object-oriented extensions was that they had become bogged down in a state-based view of specification. This seemed to me to be so limiting. It was as if the developers of Z were satisfied with just aping programs. They didn't seem to be interested in going any further. I wanted more, and I am glad to see that Daniel Jackson does too.

Windows Programming

Over the years, I have always had a subconscious aversion to 'Windows programming'.  Now I know why:

In a sense, the whole history of new programming languages and class libraries for Windows has involved the struggle to reduce the windows hello-world program down to something small, sleek, and elegant. -- Petzold, Programming Microsoft Windows with C#, Microsoft Press, 2002, p. 47 (via Lambda the Ultimate).

If doing the simple things is difficult, then doing complex things must be well-nigh impossible!

Interval Arithmetic and Prolog

I taught myself Prolog back in 1984.  At the time I had a Sharp MZ-80B microcomputer which ran the CP/M operating system (like MS-DOS only slightly better).  I bought a Prolog interpreter and played around with it, using it to write a system for cataloging stock in the school science department where I worked as a lab technician.

Although I found the language intriguing, several things about it disappointed me.  One was the way it handled arithmetic.  Basically, when it came to arithmetic, Prolog just threw logic out of the window and did it in the same way that imperative languages did it.  I thought its designers had missed an opportunity here.  I had already come across interval arithmetic in volume 2 of Knuth's 'The Art of Computer Programming', the idea of which is that, instead of representing real values by single approximate numbers, you represent them by pairs of real numbers: a lower bound and an upper bound.  One of the problems with the single approximate number representation is that it almost always gives results that are approximations and hence are logically speaking incorrect.  The beauty of interval arithmetic is that it allows you to always make logically correct statements about real values.  This seemed to me to be a much more 'Prologish' way of doing arithmetic.

There is a minor complication in that, with some arithmetic operations, the interval returned is actually split into 2 or more intervals.  For example, if you divide 1 by the interval [-0.1,+0.1] you get a result which is the union of [-infinity,-10] and [+10, +infinity].  However, this can easily be handled by Prolog's back-tracking mechanism in which one of the intervals is returned first and the other is only returned if the first computation fails and back-tracks to this point again.

Nearly a decade later I came across the Motorola 68040 microprocessor and was surprised to find that it included hardware support for interval arithmetic in the form of special rounding modes (round towards plus infinity and round towards minus infinity).  Such modes are necessary to enable the lower and upper bounds to be determined efficiently.  These rounding modes were specified in the IEEE 754 standard for binary floating point arithmetic.  It pleased me that some experts thought interval arithmetic important enough to include provisions for it in a standard.  I later learnt that there is quite a lot of research in the use of interval arithmetic for certain kinds of computations.

Leonid Meteors

I woke Zoe up at 3:45am this morning and we went out to watch for Leonid meteors.  The sky was largely clear with a little thin cloud now and then.  Our observing site, the cricket pitch in Reading University grounds, was not ideal: there are sodium street lights at about 100 metres all round, but it is the best available site close to our home.  Between 04:10 and 04:50 UT we saw 8 Leonids.  Not a meteor storm but still worth the effort.  Zoe seemed pleased, anyhow.

The Fundamental Forces of Nature

A question from the Jefferson Lab's "Who wants to win a Million Dollars?" quiz:

Which of the four fundamental forces of nature is responsible for keeping you on the earth's surface?

A. The strong force

B. The weak force

C. The electromagnetic force

D. Gravity

The intended answer is D, gravity.  However, this is not correct.  We are kept on the earth's surface by two forces: gravity presses us down, but we are also prevented from falling through to the centre of the earth by electromagnetic forces between atoms in the ground.  It is the balance between these two forces that keeps us on the earth's surface. It's very easy to take for granted the solidity of the ground we walk on.

The quiz question could easily be fixed by inserting the word "down" thus:

Which of the four fundamental forces of nature is responsible for keeping you down on the earth's surface?