Archive for 2nd January 2010

Is program proving viable and useful?

Is program proving a viable and useful endeavor? Does it create more problems than it solves?

Today I participated in a reddit discussion thread. The discussion brought up some issues I care about, and I think others will care also.

Although I’m quoting from another person whose viewpoint may contrast with mine, I mean no insult or disrespect to him. I think his views are fairly common, and I appreciate his putting them into writing and stimulating me to put some of mine into writing as well.

[…] you could specify the behavior it should have precisely. However in this case (and in most practical cases that aren’t tricky algorithms actually) the mathematical spec is not much shorter than the implementation. So meeting the spec does not help, the spec is just as likely to be wrong/incomplete as the implementation. With wrong/incomplete I mean that even if you meet the spec you don’t attain your goal.

I like the observation that precise specifications can be as complex and difficult to get correct as precise programs. And indeed specification complexity is problematic. Rather than give up on precision, my own interest is in finding simpler and clearer ways to think about things so that specifications can be quite simple. Thus my focus on simple and precise semantic models. One example is as given in Push-pull functional reactive programming. I’m proud of the simplicity of this specification and of how clearly it shows what parts of the model could use improving. (The Event type doesn’t follow the type class morphism principle, and indeed has difficulty in practice.) And since such semantics-based software design methods are still in their infancy, I agree that it’s usually more practical to abandon preciseness in software development.

For more examples of formally simple specifications, see the papers Denotational design with type class morphisms and Beautiful differentiation.

I suspect the crux of the issue here is that combining precision and simplicity is very difficult — whether for specifications or programs (or for many other other human endeavors).

Any intelligent fool can make things bigger and more complex … it takes a touch of genius — and a lot of courage — to move in the opposite direction. – Albert Einstein

We had been writing informal/imprecise “programs” for a long time before computers were invented, as various kinds of instructions/recipies. With mechanization of program handling in the 1940s came the requirement of precision. Since simple precision is difficult (according to my hypothesis), and precision is required, simplicity usually loses out. So our history of executably-precise programs is populated mostly by complexity.

I conclude that there are two ways of constructing a software design: One way is to make it so simple that there are obviously no deficiencies, and the other way is make it so complicated that there are no obvious deficiencies. The first method is far more difficult. – C.A.R. Hoare, The Emperor’s Old Clothes, Turing Award lecture, 1980

As much as one assumes that the future is bound to perpetuate the past, one might believe that we will never escape complexity. In my own creative process, I like to distinguish between the notion of necessarily true and merely historically true. I understand progress itself to be about this distinction — the overturning of the historically true that turns out (often surprisingly) not to be necessarily true.

What about specification? Are precise specifications necessarily complex, or merely historically complex? (I.e., must we sit by while the future repeats the complexity of the past?) This question I see as even more unexplored than the same question for programs, because we have not been required to work with formal specifications nearly as much as with formal programs. Even so, some people have chosen to work on precise specification and so some progress has been made in improving their simplicity, and I’m optimistic about the future. Optimistic enough to devote some of my life energy to the search.

Simplicity is the most difficult thing to secure in this world; it is the last limit of experience and the last effort of genius. – George Sand

Everything is vague to a degree you do not realize till you have tried to make it precise. – Bertrand Russell

I expect that future software developers will look back on our era as barbaric, the way we look at some of the medical practices of the past. Of course, we’re doing the best we know how, just as past medical practitioners were.

I know people are apt to hear criticism/insult whether present or not, and I hope that these words of mine are not heard as such. I appreciate both the current practitioners, doing their best with tools at hand, and the pioneer, groping toward the methods of the future. Personally, I play both roles, and I’m guessing you do as well, perhaps differing only in balance. I urge us all to appreciate and respect each other more as we muddle on.

Why program with continuous time?

For me functional reactive programming (FRP) has been mainly about two principles.

One is denotational design (i.e., based on simple, precise denotational semantics), which has been integral to FRP since the first incarnation as ActiveVRML. I’ve written several things recently about denotational design.

My second core principle is continuous time, which has been present since Fran & ActiveVRML’s predecessor TBAG.

Today I read a confusion that I’ve heard many times before about continuous time, which I’d like to bring up, in part because I love continuous time, and in part because there’s a much broader underlying principle of software design.

[…] I don’t see why the lack of continuous streams leaves a “gap”. In the end all streams are discrete.

“In the end”, yes. Just as in the end, numbers are displayed as ascii numerals. However, programming is more about the middle than the end, i.e., more about composition than about output. For that reason, we don’t generally use strings in place of numbers. If we did, composition operations (arithmetic) would be very awkward. Similarly, continuity in space and in time is better for composition/modularity, leaving discreteness to the output step.

Another name for “continuous” is “resolution-independent”, and thus able to be transformed in time and space with ease and without propagating and amplifying sampling artifacts.

As another example, consider the data types in a 3D graphics API. In the end, all graphics is pixels, isn’t it? So what gap is left in a pixel-oriented API that doesn’t address higher-level continuous notions like triangles or curved surfaces? (Hint: it’s not just speed.)

One could go further than strings and pixels, and say that “in the end” my data types will end up as phosphors or electrical impulses, so programming at those levels is perfectly adequate. Again, composability would suffer.

Another example is functional vs imperative programming. It’s all side-effects in the end. Functional programming excels in composability, as explained and illustrated by John Hughes in Why Functional Programming Matters. And I’m not just talking about pure functional programming, but the availability of compound expressions, as introduced in Fortran (controversially), despite that machines just execute sequences of atomic, side-effecting statements in the end.

Another example, and really the heart of John’s paper, is finite vs infinite data structures. We only access a finite amount of data in the end. However, allowing infinite data structures in the middle makes for a much more composable programming style.

Some unsolicited advice to us all: Next time you see someone doing something and you don’t understand their underlying motivation, ask them. Many issues are not immediately obvious, so don’t be shy! Reading papers can help as well.

For more on continuous time:


  • 2010-01-03: Trimmed & tweaked the unsolicited advice. Hopefully less peevish/patronizing now. Thanks for the feedback.
  • 2010-01-07: Trimmed quote.