1 + 1 = 2

Over at The Universe of Discourse, Mark Dominus has a nice article on Whitehead and Russell's Principia Mathematica from the viewpoint of a modern computer programmer.  One quotation:

... The notation is somewhat obscure, because mathematical notation has evolved substantially since then. And many of the simple techniques that we now take for granted are absent. Like a poorly-written computer program, a lot of Principia Mathematica's bulk is repeated code, separate sections that say essentially the same things, because the authors haven't yet learned the techniques that would allow the sections to be combined into one.

Are Tests really Specifications?

Martin Fowler, Jeff Langr and Bob Martin seem very keen to defend the idea that tests should be regarded as specifications.  To me, this seems very strange, almost bizarre.  

Don't get me wrong, I recognize the value of automated test suites, but it never occurred to me that anyone would regard them as specifying the software they test.  This idea seems to show a fundamental misunderstanding of the relationships between specifications, programs and tests, and it blurs important distinctions.

Fowler uses the term 'Specification by Example'  but what he is really talking about is exploring the specification by generating examples.  This is a good and valid activity, but it think it is incorrect to call the generated examples the specification. 

The exponentiation example that Langr presents is great as a suite of tests, but as a specification it is rather a poor one.  Firstly, it is Java-specific (it would have to be rewritten to apply it to a Python program) but the concept of exponentiation is independent of any programming language.  Secondly, although Langr criticises the Sun specification for being too long, his is about the same length and doesn't even cover floating point exponents as the Sun one does.  Thirdly, his specification fails to actually define what exponentiation is (this is in spite of him criticising the Sun one for the same failing).  He gives lots examples (2⁴ = 16, (-2)³ = -8, and so on), but these do not amount to a definition.  If you want to define exponentiation you really have to use equations, for instance: a⁰ = 1, aⁿ = a*a^n-1 and so on.  Incidentally, this enables you to define floating point exponents in terms of integer exponents quite simply by using the equivalence between between y = a^m/n and y^m = aⁿ (for example:  y = 10^3.14159 is equivalent to y¹⁰⁰⁰⁰⁰ = a ³¹⁴¹⁵⁹).

Fowler, Langr and Martin seem to be trying to use 'Tests are Specifications'  to support Test-Driven Design (TDD).  I think this is a mistake on two counts: firstly, tests are very poor specifications and, secondly, TDD does not need this support - it stands perfectly well without it. 

Calling tests 'specifications' is contrived, misleading, and devalues the concepts of specification and testing.  Why then should obviously very intelligent and experienced people want to do this?  I can only assume that it is a result of political forces within the XP/Agile movement.  Maybe their clients asked for written specs, so the Agilists looked around for the nearest thing that they actually do write, found tests, and decided to call them specifications.

Poor Abstractions as a cause of Software Failures

From Software Abstractions - Logic, Language and Analysis by Daniel Jackson (MIT Press, 2006):

The case for formal methods is often based on the prospect of catching subtle bugs that elude testing.  But in practice the less glamorous analyses that are applied repeatedly during the development of an abstraction and which keep the formal model in line with the designer's intent, are far more important.  Software, unlike hardware, rarely fails because of a single tiny but debilitating flaw.  In almost all cases, software fails because of poor abstractions that lead to a proliferation of bugs, one of which happens to cause the failure.

Beware the Optimistic Engineer

At the end of EWD500, an account of how he discovered and then corrected a bug in the On-the-Fly Garbage Collection algorithm, Edsger Dijkstra draws the following conclusion:

... for the design of multiprocessor installations we cannot rely on the traditional approach of the optimistic engineer, who, when the design looks reasonable, puts it together to see if it works.

After having just spent several weeks tracking down and fixing a bug in some multiprocessor software that I wrote myself, I now recognize myself to be an 'optimistic engineer'.  I am teaching myself to use Alloy in order to keep my 'optimism' under control.

Daniel Jackson's new book has arrived!

This afternoon I got home from work to find a letter from Waterstone's saying that my copy of Software Abstractions had arrived.  I put my shopping bags down on the kitchen table and went straight back out again and caught the bus back into town to pick it up.  Zoe had to to spend an extra 45 minutes at after-school club as a consequence. 

I have high hopes for this book, and will talk about it more when I have had a chance to go through it.  Of all the specification methods that I have come across, Daniel Jackson's Alloy is the most similar to my own ideas.  I like its simplicity and cleaness.  I now want to find out how practical and scalable it is.