A Distributed Library

To make sure not to mislead my readers for too long, in particular the programmers among them, I insist in specifying that the topic is a library made of shelves and books (remember those bunches of paper?). The idea of this essay is to explain, mostly for my own benefit but maybe for that of others, one of the interests of collecting books. Personally, I love books and, although appreciate wikipedia for what it is, I think no electronic medium can overcome the joy of possessing an extensive book collection. Once in a while, I go on a book buying spree and, although some of them have been sitting on my shelves unread, I think this habit of mine is very useful. For one thing, I read fairly slowly and, sometimes, I like to put a book back in the shelf without finishing it. For those reason, if the book is good enough, it is very beneficial to own it. On the other hand, I like to see myself as a node in a distributed library. Whenever I invite people over at my place, one of the things he or she will see is my collection of books and, sometimes, they get interested in one or two of them and bring them home to see if they like it or if they can learn something from it. It can be viewed as a means of propaganda but also as a means for education. Indeed, I think it is very convenient to be able to educate each other in an informal way and being part of a distributed library seems like an efficient way to do so. Simon Hudon July 12th, 2009 Zürich

Computer Aided ...

I made no secret that I consider E.W. Dijkstra a very wise thinker and I take many of my ideas from him. One of the things I've been hesitant to accept from him at first is his abhorrence of the use computers. It's been at least 4 months maybe as much as six months since it dawned on me that I am indeed addicted to the use of computers. There's no other ways to talk about the excessive reliance on electronic communication (e.g. looking for emails more than once an hour), my habit of browsing meaningless content on the internet and, more importantly, my habit of relying on software tools when they ofter arguably little improvements on productivity and probably some awful deterioration also. I just started reading the book "In Praise of Slow" by Carl Honoré and went through the section where he describes how in capitalist societies we made of time a new god. In other words time is more in control of our life than we are. It makes for some very nice reflections but for now, I'll come back to my main topic. In a similar way, the computer has come to possess control over our work. I can't count anymore how many times a day I get annoyed and frustrated with how my computer is working against me. It goes from simple trivia like message boxes popping up while I am typing something and forcing me to respond immediately to the use of theorem provers that relays my job to a secondary place by taking the reins passing to the use of IDE that do not work and word processors that pretend to know better than me what I want to do. In some cases, this is plain condescending but in every cases is completely harmfu to productivityl and destroys my motivation. Recently, I bought a new tool that I am pretty satisfied with. As a word processor, it does not argue with me. As a theorem prover, it allows me to keep the reins and go where I want to go. As an language editor, it does not crash and does not ship with faulty libraries. Finally, it very rarely interrupts me in my work. I bought a fountain pen and, although I still use the computer in a pretty addicted fashion, I see a change happening and I can't see how it wouldn't be for the best. In any case, the feeling is one of pleasure and satisfaction. And now, for those who wonder when it interrupts me: it's when my cartridge of ink is empty and I store two in my pen so the replacement is a fairly short operation. I am now resolute to using computer as much as possible for communicating with my loved ones which are now very far away and to question every other necessity I feel of using a computer. This is far from done but I expect some nice results. As an aside, as a software developer I think I draw an important lesson. In the same way you should never be condescending toward your readership, you should not be either towards your users. If they use the computer, they should know what they want and you should not take the control from them. For example, when forms have to be filled, you should allow the user as much as possible to fill them in one go and possibly even in the order of his choice. A good example of a violation of this principle is the setup of Windows where installation sequences are interspersed with questions so the user has to sit through the whole process. Simon Hudon 12:55 AM on July 12th Zürich during a sleepless night

On Programming Languages

Sometimes, some programming languages popularize powerful ways of thinking about a problem. It is not too rare however that a language would create popular way of obfuscating a problem. APL and C++ are an example of the former. The difference between the two is that C++ allow you to believe you actually understand the problem when you don't have a clue about it. On the other hand, I have never met anybody knowing APL that claimed to be able to read an APL program. Simon Hudon July 10th 2009 Zürich

Nice Quote and Comments about User-Friendliness

"Build a system that even a fool can use, and only a fool will want to use it." I have encountered very often the notion that user-friendliness is the quality of being intuitive or, put in Dijkstra's words, the quality of "appealing to the uneducated". It seems that Microsoft can be very active in that respect. Take Word for example, it is sold with the pretense that you don't have to learn to use it but, invariably, you'll have to get accustomed to it and get an intuition of the heuristics used to justify one or another behavior. In other word, because there is the clear criteria guiding the behavior of the system that can be written down, it is believed that you don't need to understand anything to use it. If user-friendliness is to have a non condescending meaning, I would associate it with the simplicity of the design of the system and of its interface. It is acceptable to have to learn how to use a system but the description should be as short and as precise as possible. To those who believe those to be contradictory qualities, I refer to the manual of the Algol language and conclude with a quote by Dijkstra. "About the use of [natural] language: it is vain to try to sharpen a pencil with a blunt axe. It is equally vain to try to sharpen it with ten blunt axe". E.W. Dijkstra Simon Hudon July 10th 2009 Zürich

SH53 - Natural Deduction seen as the Turing Machine for Logical Reasoning

Reading through the chapter of mathematical reasoning in the B Book, I couldn't help but notice how much emphasis was put in using natural deduction. I strengthening the belief that natural deduction is not appropriate as it is for practical reasoning. In fact, I think it is appropriate to compare it to Turing machines. When we are interested in the power of a system, we want to reduce it to its bare essential. In that sense, the few simple inference rules usually associated with natural deduction are very helpful. But we must keep in mind the bias that we have when delivering that judgment: we are doing the job of a logician who wants to compare different systems. It is the same for Turing machines. They are very simple and this is why it helps reasoning about their computability properties. I think nobody knowing anything about programming would suggest to use a Turing machine to build any kind of useful system unless it is sufficiently small as to be of no significance.

Similarly, I don't think that using natural deduction as a means for reasoning about systems is any wiser than programming with Turing machines. For simplifying the logic, natural deduction offers no means to exploit equivalence because it can be dealt with using implication. It is true but not helpful when carrying out an actual reasoning. Keeping equivalence intact is simply much more efficient. People don't have to go through the same proof twice. It is also true that even if case analysis can help achieve the proof, it also helps making it unmanageable.

In short, developing proof design techniques is as necessary as developing program design techniques and, similarly, it involves developing the right notation and finding powerful heuristics. Natural deduction is not a means to that end. However, it can be used to prove properties of equational logic without to need use it when carrying out the actual reasoning.

Simon Hudon Zürich June 9th, 2009

SH48 - Weakening Preconditions

I remember an instant messaging conversation I had with Prof. Jonathan Ostroff (YorkU) where he said he was buying more and more the view of preconditions as waiting conditions like in Event-B and SCOOP. I objected that, obviously, unlike Event-B, we can't hold the position that preconditions must be strengthen. It was, as I thought, some kind of law of nature and common sense that only postconditions can be strengthened. Preconditions can only be weakened. But what if it does not fit the essence of object oriented programming? Certainly, it is acceptable that the precondition of routines be weakened in the process of refinement. Since features in classes are implemented as routines (whenever they use arguments), why not just carry over the rule to the implementation of class features?

The fact that they are type bound makes an important difference. Rather than understand that the target of a call is just another kind of argument to a routine that will be dynamically chosen so that it meets (in a semi-formal way) the specifications of the routine, it should be understood as an event that occurs that (might) transform the current state of an object. That event can be or not provoked by a certain client. Whenever it is, it does not matter for the correctness of that client that the precondition gets weakened in the refinement of its supplier. On the other hand, since object aliasing is an important part of object oriented programming, considering the transformation of an object by other clients makes sense as the general case. If we assume that no other clients will invoke a certain feature unless its guard (or precondition) is satisfied, weakening it might produce surprising results. On the other hand, if we allow ourselves to blur the distinction between a class and an event-B abstract machine, we might want to make sure that the deadlock condition of a module is not strengthened in its refinements. It would mean that, in any refinement, if the guard of an action is strengthened, it must only be in the context of an action split where the guard of all resulting actions complement each other in a way that their disjunction is equivalent to the guard of the refined event.

The door does not seem to be completely closed for the notion of precondition weakening but I, for one, would not dwell on it.

Simon Hudon May 18th 2009 ETH Zürich

SH16 - Sacrificing Efficiency for Some Degree of Confidence

Is the concern for software correctness getting in the way of efficiency? or Sacrificing efficiency for confidence (as opposed to correctness)

Post-scriptum note: the opposition between correctness and confidence is based on the objectivity of the criterion of correctness and the subjectivity of the criterion of confidence. Confidence can be the result of obliviousness.

Also, I have not reread it since posting it on my blog and it might need some moderation. (End of note)

With modern trends like test driven development, it seems like, for the sake of having a testable system, one will always (or most of the time) take the shortest path allowing him to add just one feature. It is positive to see that he always worry about having something that works, albeit using very restrained notion of what a "working system" is. However, the fact that the modern programmer (or, to borrow a more trendy term, the average programmer) is unable to reason in any effective way about the formulation of his specifications or even those of his architecture makes him unable to postpone the implementation until such a time as his design has been validated on its own. This points out to a blatant lack of separation of concerns. A more disciplined approach would require that the programmer be able to validate his architecture using nothing but the information contained in it and the information contained in the formulation of the relevant requirements.

It is very important to make precise what is meant by validation. Like the term coined for any profound notion, it has been used to designate so many different concepts that, it cannot be understood as anything more than a buzz-term unless it is explicitly defined.

The validation of an architecture means that any implementation following its rules is bound to produce correct result for every valid input. This means that it is a validation impossible to accomplish using testing. Some might argue that model checking would be a valid choice to come to grip with that separation of concern. If we forget everything else, they could be right. The problem with model checking is that we still rely on a posteriori verification: the concern for correctness still fails to guide the programmer to his solution. Proponents of the notion of the "average programmer" might be satisfied with that since they accept that the layman has, at best, a third rate intellect and we cannot ask him reason in any formal way about his work. However, it is clearly a better approach than postponing any kind of validation until after an implementation has been provided.

What I'm coming at now is that since the implementations are rushed at, programmers don't seem to take any care for making it efficient or correct in a general way. All that is expected is that the test suite passes. If any efficiency issues arises (much later in the development) it is considered that it is the good time to address them. It seems that an efficient implementation would have been easier to produce at the very first moment that the programmer started writing it.

Simon Hudon Gatineau, December 2008 continued in Zuerich, May 2009