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.

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