A discipline of programming

| categories: thoughts

Classic Dijkstra:

Sad remark. Since then we have witnessed the proliferation of baroque, ill-defined and, therefore, unstable software systems. Instead of working with a formal tool, which their task requires, many programmers now live in a limbo of folklore, in a vague and slippery world, in which they are never quite sure what the system will do to their programs. Under such regretful circumstances the whole notion of a correct program – let alone a program that has been proved to be correct – becomes void. What the proliferation of such systems has done to the morale of the computing community is more than I can describe. (End of sad remark.)

This is from "a discipline of programming" which, besides being a clear tutorial on Dijkstra's formalism, is one of those books that changes how you think about solving problems – and about computation in general. You need to be comfortable with mathematical and symbolic language, but it's worth the time and effort.

I can't fully get behind Dijkstra's stringent, almost ascetic approach to programming. It's clear that we can achieve a lot without formal methods, and that until we have powerful language support, it will be hard to use serious formalism successfully in projects of the scale we habitually undertake now. Nevertheless, he's one of my heroes. We need these extreme and deep voices to remind us that despite our accomplishments, we're at the very beginning of all this and we have a long way to go.

I highly recommend browsing the E. W. Dijkstra Archive. Dijkstra believed in maintaining a lively correspondence with his peers, and his EWDs make great reading.

"But what good are formal methods? You know, in many cases, formal methods are just rubbish. Sometimes one gains more from simply having a friendly chat. Oh, the formal methods will always be with us, sir, you may be assured of that; but what good are they, in the last analysis, I ask you?" – Porfiry Petrovich, from "Crime and Punishment".

Computation, space and identity

| categories: thoughts

I've been thinking a little about computation, the spaces in which it operates, and its social and psychological impact.

In "A Secular Age", Charles Taylor discusses at some length the idea of the buffered self. He says that premodern people had a more porous identity. There was a sense that external forces could affect, possess or modify you ‐ a spirit, or a curse, or even a physical object (e.g. a relic) imbued with some power. In contrast, modern people have an identity that is highly internal and much less thoroughly penetrated by a real or imagined spiritual world. This is interesting, though I'm not sure that Taylor presents enough argument to convince me.

Computation can be viewed as giving us access to an abstract space. In a sense it has always been there and accessible to us, but slowly and with little effect. Computers link us to this space. They allow us to rapidly manipulate it, create structures and processes there, and use them to drive change in the physical world.

A program text generates a computational process. It's a precise description, in esoteric language, of the steps we want this process to take. A small program text can generate a process that in turn creates and manipulates giant, complex data structures, and can do so more or less indefinitely. In today's warehouse-scale computers it can do so across hundreds or thousands of individual physical machines; with the complex interleaving of client- and server-side computation used by modern web applications, a typical action like opening and reading an email results in intricate cooperation of hundreds of different communicating processes.

A prevalent metaphor carried through the literature and culture of computation is the process as a spirit summoned from the machine. This is unsurprising: the tireless daemon is constructed from pure thought and energy by weird incantations and does exactly what you tell it to, often with unintended consequences. Those consequences can range from mildly annoying to catastrophic, depending on what parts of the physical or social world we grant our machines the power to affect.

Today many people are carrying pocket computers: machines linking them to the global network of machines ‐ and beneath the slick user interfaces and endless applications, the unfamiliar spirit world of communicating computational processes. These computers are physical objects imbued with the power to make us glittering social hubs or dumb absences. I wonder to what extent these are modern relics, and to what extent people interact with them superstitiously ‐ always holding them just so or performing operations on the interface in the right order because otherwise those unruly spirits seem to misbehave. I wonder how close they come to penetrating our buffered selves and making us believe in magic.

« Previous Page