On being formal, and possibly agile too...

Way back in my past I used to research formal methods for software engineering. Actually I still do, though now most of my time is actually using formal methods to make better software.

Formal methods are nothing more than a collection of languages and techniques for modifying and reasoning about things (models) written in those languages. Some of these techniques encompass how the process of building a system is made. Herein lies one of the first problems encountered by formal methods practitioners and that is the almost constant challenge from some, such as many in the agile community, that seem to be religiously against any form of modelling.

To those who believe that code is the only deliverable and the only thing that matters, well, C++, C, Fortran, Clojure etc are all formal languages, and you're probably using many of the techniques from formal methods right now as your write your code.

Language such as B, Alloy, Z, VDM etc do is provide a method of expressing a model without worrying about certain, awkward details of their implementation or execution.

Indeed what is happening here is that we have languages and techniques that allow you to concentrate on reasoning and thinking about the problem you are trying to solve without getting bogged down in the details of the final implementation.

If your first worry is the implementation language, or the operating system, or which libraries to use, etc, then you're most certainly not solving the problem.

At Nokia we had some very great successes using formal methods in an agile manner for the development of a semantic web infrastructure for the "Internet of Things". Concentrating on what the system had to do and then later worrying about how it was implemented meant that when it did come to the time we needed to architect the components and decide on specific implementation issues we already knew how the system was going to work, what tests we would need to run and what the expected answers were going to be.
Indeed, many of the tests were little more than checking that the code behaved the same as our earlier models - regression testing if you like.

This resulted in a huge decrease in the time spent in coding and the effective removal of nearly all (logic) bugs before even the beta releases. In fact most of the bugs turned out to by typos.

Furthermore, when it came to updating the software with additional features, instead of blindly bolting on a new use case we could reduce most of the new feature requests down to library or convenience functions over the core functionality rather than complicating the design with those "new" features.

This latter point is very important in that even though there is pressure to constantly add new features  (and the Pareto Principle applies here), most new features are really just convenience functions that already exist in the software.

I even remember one system where management demanded so many new features (all specified as their own use cases) that the system actually ended up implementing not only the same feature many times but features to disable the requested feature...

Ultimately formal methods is a discipline of thinking, rather than any technique to develop software. Just as much as Agile is a discipline of development.

To use formal methods does not mean any form of top-down or Waterfall development, it does not mean that one has to use refinement or a language like B or Z or VDM or Alloy etc. Just the simple act of writing a precondition to a function in C, or expressing a simple class diagram in UML, or ER diagram to explain a database schema (SQL or NoSQL) to demonstrate the workings of a system, or to clarify what something mean IS being formal.

The best agile developers I have seen all have formal methods backgrounds. The reasoning is that they already have the discipline and education and the tools to think and reason about their system, even if applied implicitly. Agile depends upon great communication between the developers and the customers and giving those customers exactly what they need in a manner that avoids technical debt (viz. situational awareness).

Whether we like it or not, great software engineering comes from understanding how our craft works at its most fundamental levels - imagine civil engineering without the mathematics of physics (a classic example), or even ballet without an understanding of human movement?

References:

[1] Ian Oliver Experiences of Formal Methods in 'Conventional' Software and Systems Design. FACS 2007 Christmas Workshop: Formal Methods in Industry. BCS London, UK, 17 December 2007 

[2]  Ian Oliver Experiences of Formal Methods in 'Conventional' Software and Systems Design

Formal Methods in Conventional Software Development Environments from Ian Oliver

More ballet and software engineering

Sometimes a quick search using some popular search engines reveals people with similar ideas, in this case about ballet and software engineering: on the IBM Developer Works site is an article dated from 2005 by someone called "gbooch"*:

Software architecture, software engineering, and Renaissance Jazz

which mentions the link between software architecture and dance:

"It seems to me that there's a curious relationship between dance and software architecture: in both disciplines, there are only a limited number of patterns available, each genre assembles those patterns in specific ways that define a particular genre, and furthermore, most knowledge is passed on through tribal memory, from one dancer or architect to another. In dance, by the way, some attempts have been made to define a graphical notation for describing dance movements, just as we have the UML for visualizing, specifying, constructing, and documenting software-intensive systems."

Exactly...!

*I guess if the mysterious "gbooch" thinks this then I'm in good company.

Then there's another post on Techtalk: If Software Were Like Ballet which lists a number of points, the first of which is:

• Little kids are encouraged to get used to the equipment and basic practices.  Even if they don't actually do these things they are told about build and release cycles, software qa, and algorithms.

Now I don't agree with some things said in that posting, but certainly the above at least in terms of encouraged to use the correct equipment, techniques and basic practices is apt.

The Ballet-Software Engineering "Isomorphism"

A grand title for some thoughts. After watching a dance show involving various styles of dance etc a thought struck me on some interesting parallels I see between dance and the practice of software engineering. I guess this comes from reading things such as Baez and Stay's "Physics, Topology, Logic and Computation: A Rosetta Stone" - a paper describing the links between various scientific disciplines, ostensibly through category theory.

As I and many others have stated before the key to good software engineering (and thus great software) is an understanding and use of the core, formal theories of computer science - I consider software engineering to be a sub-discipline of computer science (and in turn mathematics). Why should this be so? Simply because of understanding how each of the parts of a piece of software interact and an appreciation of the complexity and need for elegance and simplicity in this.

So what has this got to do with ballet? Comparing modern dance with ballet and the dancers performing their routines I noticed the approach to the task was in most cases different - there is an interesting exception which I'll get to later. The difference was in the execution, fluidity and attitude to the performance: how accurate the moves were being performed individually and collectively as a group. An interesting point I thought was that you could recognise the really talented dancers by how they looked at each other and the audience.

Modern dance seems to be (or is) very free in terms of movement, style and composition - akin to agile methods in software engineering. In some ways, modern dance is easy ... anyone can just move, similarly to agile methods, anyone can hack a project together. But to get a consistent, fluid, elegant whole is extremely difficult in that the choreography of the individual dancers becomes very difficult to make consistent, unless the dancers are very experienced and instinctively understand how each is moving relative to oneself. I suspect the very good dancers here have or understand the fundamentals of movement to a very precise degree.

Ballet on the other hand is very strict with a limited set of movements which themselves are precisely defined. Wikipedia's (sorry, I know you shouldn't cite wikipedia!) article on ballet contains the statement:

"It is a poised style of dance that incorporates the foundational techniques for many other dance forms."

I need say no more regarding the basis of ballet for other forms of dance.

An in that respect we have our link with mathematics, computer science and software engineering. Formal methods are computer science's version of ballet: strict rules and technique and hard to master but forming the basis for the rest of the subject, especially software engineering.

When auditing, watching or even performing the "art" of software engineering - or at least - developing software (and systems); those who have an understanding (either explicitly or implicitly) a deep understanding of how the science works build the best software. The "moves" of the software engineer are deliberate, planned and executed with precision. This remains the same whether this is agile or formal development, though most agile development tends to be very ad hoc, messy, immature and poorly executed - like the modern dancer without discipline.

And indeed this is the core of what makes a good engineer - not whether they have the formal grounding, but they have an understanding of what makes the engineering work and the discipline to actually use those techniques properly.