Joseph Goguen authored Algabraic Semantics of Imperative Programs, and was professor of computing systems at Oxford. Given those credentials, one might expect him to have been firmly on the “formal methods” side of programming language research. But in an essay in Software Development and Reality Construction _entitled “_Denial of Error“, he wrote this:

In proposing methodologies to guarantee the absence of error, we deny the incredible richness of our own experience, in which confusion and error are often the seeds of creation; in this way, we limit our own creativity.

Edsger Dijkstra was one of the principle instigators of the “formal methods” and school of thought. Specifically criticizing the “Dijkstra School”, Goguen writes:

Perhaps not unexpectedly, this “wp calculus” requires significant human “intervention” at exactly the most difficult points, namely the loops. And for most programs that go much beyond the trivial, the insights needed to write the loop and variants are tantamount to already knowing how to write a program; moreover, these insights are more difficult to achieve in the wp calculus and they would be more operational context.

Indeed, I have seen good students who had been taught that the wp calculus was the right way to program, become so discouraged over the difficulties that they experienced, that they came to believe that they could never learn how to program and should therefore seek some other profession! In general, such a rigid top-down ideology inhibits experimentation, the exploration of tradeoffs, accidental discoveries, and so on. Moreover, it can be harmful to students, wasteful of time, reinforcing of an inflexible view of life, and inhibiting two intuition and creativity.

Later clarifying that he believes formal methods _do _have a place, Goguen goes on to say:

…rather, I am criticizing the tendency to apply formal methods in a rigid, top-down hierarchical manner. In fact, I believe that if appropriate formal methods are used in a flexible, non-ideological way, they can lead to better programs, with greater efficiency, and fewer bugs.

But bugs are inevitable. If they don't occur in coding, they will appear in design, specification, requirements, or use. […] Of course, no one wants bugs, or wants to spend any more time than necessary on debugging, because it is difficult and unpleasant. But nevertheless, bugs are interesting and important in themselves: they define the boundary between what is understood and what is not. Hence, they show us where our weaknesses are, and provide opportunities for us to learn and grow.

Personally, I'm concerned that “Dijkstra School” approaches to error appear altogether too reminiscent of the TSA: spending endless time in asking “how can we restructure the system so that this error could not have happened in the first place?”. A point of view focused on prevention, and on categories of error we already understand, will necessarily shortchange the tools and methods for approaching brand new new surprises as they happen.

I want programming languages in which errors constitute rich, interactive playgrounds for undirected, creative discovery. Where context is valued, preserved, and readily examinable, and where the system is an assistant in event correlation, rather than a snickering opponent.

Based on musings originally published in SIGAVDI#004, November 2, 2015. March 2020 update: lately I've been playing with Dark, whichstrikes an interesting balance between formality and rich error context.