Where have I been?

It has been a while since my last blog post. I have a collection of posts that I have been meaning to posts but that were somehow never good enough. I'm going to try harder to publish them. In the mean time, here is a snapshot of what has been going on with me in the last two years... at least scientifically.

I underwent a peculiar transformation since I moved from Zürich to Toronto. I used to think that you can study a software system purely from a logical point of view and, when you proved all you needed to prove, all is left to do is run the software. I have done it for some non-trivial software system but I realize that, for a bigger piece of software, the amount of work to cover the whole thing would be excessive both in the sense of "exceeding necessity" and "exceeding ability to do so". I'm reworking my vision of software design as an activity that includes proving theorem but which also comprises other techniques of validation. For example, random testing as done by QuickCheck in Haskell is often a good compromise. The key is to choose which technique applies best.

For instance, I started developing a program one year ago and it has now become relatively big (considering that I'm the only person developing it) and, to my surprise, it works well even though I didn't prove a single property about it. In the back of my mind however, I keep pulling some parts of the design aside and figuring out the logic that would make it possible to prove that it is correct. One of these days, I'll prove the correctness of some crucial parts of my programs and I think that will be both really interesting and really useful -- especially considering that the program is a formal verifier.

On the other hand, I am also discovering the interplay between mastering the theory and having good software tools for designing software. I used to think that if you know the theory well, you have no need for tools. I'm realizing that this is a pretty silly point of view: the program that I mentioned above is specialized in writing proofs for simple conjectures. It very incredibly fast. In one of the small systems that I use that tool for, there are around 500 conjectures that need to be proved. Most of them are incredibly easy to prove but they still need to be proved. My tool takes about 30s to prove 499 of them leaving me with the truly difficult theorem. That's incredibly helpful because now, I can focus my attention on the hardest of the hard design problems. The best part is, compared to an interactive prover, I do not need to manually invoke the prover on each proof obligation. They will all be attempted automatically except for those with a proof provided by the user.

The tool is designed to allow me to verify Unit-B models. I don't think I would be able to use Unit-B as confidently as I do and as efficiently as I do without it. Even better, when using Unit-B to develop the very first examples, every time I was faced with a problem, I could improvise a solution and think really hard and figure out that it was valid. This is very inconvenient to teach the method because I hardly have a list of all the tricks that I use. By implementing a verifier, I need to identify the truly useful techniques and make sure that they can be used with confidence and have a clear explanation to disallow whatever I choose to exclude. In other words, I'm now forced to formulate the rules of the method independently of any one example.

So much for simplistic views of the world.

Bad Separation of Concerns

In the course of my master's, I have to attend a seminar and prepare one talk. Last week, the talk I listened to was about using pattern matching in object oriented programming languages. I thought, as the talk went on, that all the yardstick they took to evaluate the design of their language construct was all wrong. It struggled, in my opinion in vain, to improve the expressiveness while retaining the best possible performances and remaining "concrete". In that respect, I tend to take for granted the necessity of expressing precise specifications with every piece of code. This means that, for me, the most important is that my specification language be expressive enough, but still very simple, to allow me to reason about my problems and my implementation language be as simple as possible and allow me to express any algorithm I wish. In my experience, the specification language should involve as little operational elements as possible for simplicity. As for the implementation language, it should be possible to implement it on any reasonable architecture. Before I'm objected that it is not customary in industry to use precise specification notations or to keep multiple representations, at different degrees of abstraction, of a single solution, I have to point out that this is an academic result and it does not have to follow industrial customs. Actually, I would go one step further and state that, if, in academia, we wait for techniques to become widely adopted before using them, we are lagging behind and risk doing no more than producing more of the same. Academia being more remote from the market place than industry are supposed to be less affected by the political issues that keep industry behind the state of the art. And this is not badmouthing the industry: it is understandable that they have more concerns than only technological ones. Let's get back to the paper. In their design, they seemed to tackle both problems of expressiveness and implementation at once and the result was not pretty. For example, in their pattern matching, they had to take into consideration that the evaluation of the expression (which, in their case, is an absolute necessity) they were dealing with could very well have side effects and this was an important concern of theirs. I think that this possibility was popularized by C and I think this is an important set back with respect to allowing programmers to think about their programs. I think, already, the discipline of separating queries from commands, which is part of Eiffel's style, is much better in this respect. They also had to deal with constructors in order to match objects like you would in Haskell. This is very ugly. Pattern matching is a very elegant way of writing expressive specifications but object creations do not fit in it. This is because an expression creating an object has an implicit reference to memory allocation and it can't be dissociated to it. People can't forget that the object has a memory representation and that a comparison in the context of pattern matching will have a given cost. I prefer to use mathematical expressions to express the value contained by the object and allocate the object only if necessary.

Aside In a recent programming experiment where I derived my code from its proof of correctness, I was parsing a string and, since all the properties of a language can so elegantly be formulated in terms of strings of character, I used strings to represent the state of the computation. I had my input string S, the processed string x and the left over string z and they were linked by the invariant:

S = x ++ z

with ++ the string concatenation operator. At each iteration, I split z in two parts such that

z = [ y ] ++ w

and scanning one character was encoded as:

x, z := x ++ [ y ], w

If you can't help yourself and have to imagine the memory footprint and performances of this algorithm, you might be scandalized that this is really inefficient. This is not meant to be executed as such; it is only a very simple way of understanding defining what the algorithm does. With one data refinement, I went to a representation where the use of memory is limited to the array representing the input, an integer index indicating which character y is and two booleans to represent the acceptance state of the algorithm. There is no efficiency problem with that, and my proof of correctness and my proof of data refinement are very simple and I consider them the clearest documentation for the algorithm.

end of aside

In summary, I think the right way of seeing that problem is:

Pattern Matching is a power way of associating properties or code with the shape of the data and we need to be able to express it. Since we can use it with code, it would be important to have programming techniques to make the executable, that is, techniques usable by a programmer to transform a specification using pattern matching into executable code implementing it. If the methods are especially effective and simple, we could have it implemented in our compiler but this is far from being a design consideration for the construct.

* * *

More recently, in my compiler design class, we were presented a research programming language which is said to be "relationship-based". I think the idea is a good one: they factor the inter-class relationship out of classes to treat them as separate modules. The question whether each such relationship deserve its own module is worthy of debate but, for now, what bothers me is that they treat it as a programming language construct, that is to say they keep an "implementability anchor" in their heads while they design the notation. One of the consequence is that they will refrain from adding anything for which they aren't sure they can compile it automatically. I would rather see this emerge as a specification structuring artifact and see some programming techniques emerge in connection to it so that the most common one can be implemented quite straightforwardly. For the rest, it's open to experimentation and, in all cases, a case by case implementation would allow optimization that systematic compilation wouldn't be able to do.

I think the big problem here is still the taking of current practices as a guideline for academic research: "since programmers don't write specifications, we won't provide a means to write good specifications even though progress would require it". I put it in my "more of the same" bin, look at the original ideas and forget about the language. Actually, I will do so when my semester is over.

Simon Hudon

ETH Zürich

finished on November 18th

Modeling vs Programming vs Coding

I usually adhere to Dijkstra's and Morgan's view of programming: it's the action of passing from a precise specification to an executable program. I've had some contacts recently with the Chair of Programming Methodology recently and I was expecting them to have a similar view to mine on what constitutes programming. I was a little disappointed to see that their view was more closely related to "writing down executable code" than "reflecting on the design of a suitable implementation for a given specification". What they call programming, I would rather call coding. Before that, I had a short talk with Dr. Jean-Raymond Abrial, founder of the B and Event-B formal methods where I saw that he shunned programming. However, I came to realize that what he called programming was also coding. On the other hand, he called the activity of central importance to software engineers "modeling" which is a term I have been trying to avoid for some time, now, because of its central role in methods like UML, which I find eminently ignorable for software engineers; it simply seems to stem from confusing vagueness with abstraction and I think there's no reasons to accept vague documentation for a design. I still prefer the word programming for the formal derivation of implementations but I feel more and more like I will have to find a substitute because of the lexicon associated with programming. It is associated with programs which is related to routines and sequential execution whereas I believe that sequential vs parallel execution is an implementation choice that should not receive half of the importance that it is usually given in the development process. To be absolutely unambiguous, I could rename the activity "designing a software system" taking the liberty of changing software with discrete if necessary but it might be a bit too long. However, design is an activity so widespread that it does not feel appropriate to use it on its own when talking about programming. For this purpose, I could resort to "modeling" but I run the risk of having to precise all the time that I have nothing to do with UML or their bubbles and arrows techniques. Ah, well! I'll keep thinking about it. In the mean time, I'll keep programming for short and design of software system to be unambiguous. Simon Hudon October 11th, 2009 Meilen

Collective Knowledge

At the moment, I have a few drafts I am writing but they are not progressing very fast and I am offering this short reflection. Looking around and reading different kinds of research, I can't help but feel that there exists a hierarchy of collective knowledge. Science is part of that hierarchy but it is not the whole story. As somebody who is strongly mathematically inclined, I have a tendency to view formal mathematics as the only means for expressing one's understanding but this position does not hold water. Since I am also very interested in methodology, namely, how we program and how we do mathematics, I have to have considerations for human activities and those are particularly hard to formalize and one might wonder what need we have of formalizing them. It must be honestly revealed that the activity of formalization demands tremendous efforts which are not carried out merely for the beauty of formal theories (although, many don't need much more motivation for doing it). The point is that, at any time before embarking on a formalization project, it is worth it to wonder if it is worth embarking on. On one hand, there is a class of programming languages, of which C++ and PL/I are nice representative, for which the formalization is not worth the effort because they are so complex and there documentation is so ambiguous that the formalization amount to reinventing them. Also, while reinventing them for the sake of formalization, for survival's sake, one should have the reflex of questioning every design decision before deciding to adopt them and, doing so, one would not end up with C++ or PL/I but with a language à la Wirth. If we carried that judgment to a further conclusion, it can also mean that they are not worth using either. On the other hand, there are subjects which are worth studying but the gain of a formalization is not immediately obvious. We have other tools than formalization to be rigorous and precise in our discourse and should not neglect them (to name only one: we have our natural language for which an exceptional mastery can do wonders). Once the benefit of formalization is seen, though, one should not hesitate. At the moment of writing, I am thinking about the general literature about programming methodology (aka software engineering). I have the feeling that although some publications concentrate on giving examples of the use of a particular method, some succeed at being very rigorous by being modest and accepting that they are merely working with one example. Also, their rigor seem to rely on the analysis of their example, of what helped and what did not. On the hand, some very disappointing papers on the topic try to be more rigorous by building a tool, having a handful of programmers use them, measure (in some vague sense) the improvement in their productivity and publish the statistic. Without a theory to compare those numbers to, they are meaningless and I can't help but see it as another instance of the general hype around statistic which I would summarize with "a number is better than no numbers at all". Simon Hudon Zürich, September 5th 2009

Algorithms in Object Oriented Programming

Approximately two years ago, I was writing a set of classes for dealing with graphs. At one point, I had to provide facilities for depth-first and breadth-first traversal. At first, I thought of doing it as a higher order function: it would be a regular encoding of a graph traversal that would use an agent --in Eiffel talk, in C# talk, it would be called a delegate-- to process every node encountered. This seemed a lot of work to set up and use and I decided to create particular kinds of cursors that would enumerate the nodes in preorder, postorder or in breath-first order. It was a very interesting exercise because I transposed the state of the computation of the algorithm to make it the state of a class. At the time, it seemed like a very nice reinterpretation of an algorithm to have it fit a more object oriented context. I did not push that investigation further. At the moment, I am working on the development of a parsing algorithm and its correctness proof. One of the decision I took was to have a token reading primitive instead of passing a complete sequence of tokens. With respect to the formulation of the algorithm, there is very little differences but with respect to its interface, the difference is big enough to allow me to do an interesting observation. The reading can be interpreted as a routine called by the program implementing the parsing algorithm, but it could also be interpreted as a method of a class whose state is described by the local variables of the algorithm. This would allow, for example, to interpret keystrokes as tokens and feed them to the parser as they come. What if we just considered it as an input without regard to whether it is ordered by a client or by the module. With that view, we could have a scanner which outputs one token at a time and inputs one character at a time. We could plug the input of the parser on the output of the scanner for which the input could either be plugged on a streamed string or on the keyboard input without significant changes. Furthermore, if we wanted to decouple further the lexical analysis and the syntactic analysis, we could put a buffer between the two (still without changing the algorithms) and we could even put each machine on its own process. Some theoretical framework which is very useful to conceive that is that of action systems. With just a few exception, an action system could be understood as a canonical view of (not necessarily terminating) programs where we have one loop over a set of one line guarded commands. For example, for the following statement: a := 32 if b > c then b, c := c, b [] b <= c then skip fi We could get the following loop which we will consider as an action system: line := 0 ;do line = 0 then a, line := 32, 1 [] line = 1 /\ b > c then b, c, line := c, b, 2 [] line = 1 /\ b <= c then line := 2 od The advantage of using an action system instead of the corresponding program (when there is a nice one) is that the action system can compose for various purposes. If you want to simulate the concurrent execution of two programs, taking the union of the actions (the lines in the loop) of their action system will give you a model of how the two programs will execute. The assertion that you put in both programs must become invariants in the loop attached to line numbers. It is similar to the methods described in the Gries-Owiki theory and in A Method of Multiprogramming by Netty van Gasteren and Wim Feijen. The other use of the action system is that it can model objects. Each action can be understood as a method or as a method call and it allow one to model "concurrent" access to objects much better than what we have with structured programming geared with type bound procedures (what we see all the time in OO languages). Simon Hudon Finished on August 26th Zürich