Formal Methods versus TDD

Back when I was taking my Computer Science degree at University I learned all about ‘Formal Methods’ (when I wasn’t playing pool, badly, that is). The main reason to use Formal Methods is to prove the correctness of programs. By stating a logical pre-condition for a block of code you can apply a sequence of logical steps to it that each correspond to the behaviour of each of the statements in the block. If when you reach the end of your block your transformed pre-condition is the same as the logical post-condition then your block is proven correct. If you do this for your entire program then it as a whole is proven correct.

So why doesn’t anyone really do this outside of academia? Basically because:

– Coming up with pre- and post- conditions that represent exactly what you want your program to do is hard

– The actual process is equally hard

– .. meaning that the whole thing is slow

OK, now flip to what I do now. I’m a big fan of ‘Extreme Programming’ techniques including Test Driven Development (TDD) which is an evolution of unit testing. Why do we do unit testing? Partly to try and ‘prove’ that each part of our program works. Its not really absolute proof since we never know if our unit tests uncover all possible bugs in the code, but its a good approximation. In fact as we add more unit tests it becomes an even better approximation of proof.

Anyway, why am I rambling about this? Well, the academic in me (which isn’t allowed out very often) always had a bit of a bad feeling about unit testing due to its lack of proof. But recently I was talking to a couple of ThoughtWorkers about analytical and numerical processes in Maths. With analysis (or calculus) you prove the answer to a problem using Mathematical logic. Some problems though are either (1) too hard to solve like this or (2) take too long to solve so you can also use numerical methods. These never give you the exact solution but through a succession of repeated calculations you can tend to (or hone in on) the solution until you have an answer that is ‘good enough’.

To me, this relationship of analysis and numerical methods seems strikingly similar to that of formal methods and unit testing. Since numerical solutions are academically valid this makes the academic in me happier about unit testing.

TDD isn’t just about testing though – its also a method of actually deciding how to write a program. You start with a failing test, write some code that fixes this test in the simplest way possible, refactor your program to remove duplication, and then repeat. In my Formal Methods studies at University I also saw how you could actually write a program based on a logical specification and a set of rules related to the ‘correctness proving’ rules. (See here). So both TDD and Formal Methods offer a way of ‘generating’ code based on testable specification (programmatic assertions for TDD, logical specifications for Formal Methods.)

In conclusion, this argument itself doesn’t prove anything (!) but in my own mind at least showing a relationship between Formal Methods and TDD strengthens the case for TDD being a valid, and valuable, technique for writing software.

Why I don't like the GAC

A real example of why I don’t like the GAC in .NET:

I’m in the middle of restructuring the CruiseControl.NET build file. I create a new build, test it and its fine. I setup a new CruiseControl instance for a project I’m working on, and that’s fine too. I then copy this instance on to the build server and it fails with a TypeLoadException.

Stripping this down, I have an application that runs on one machine, but if I copy it file-for-file onto another machine it doesn’t run. This is the kind of thing that makes the control-freak side of me’s blood boil.

My next thought is ‘so what’s different between the 2 machines?’ The only thing that effects a .NET application’s assembly load routine outside of the local directory, app configuration (which we don’t do in CCNet) and programmatic assembly loading (which we don’t do either) is the GAC. So I look in machine number 1’s GAC and I see a copy of NUnit in there. ‘Hmmm’ (I think), ‘I wonder if that’s it’ (in theory if my build had gone against the version of NUnit in the GAC vs. the directory-local one I thought I’d specified there could be a problem). So I (eventually) manage to get NUnit out of my GAC, recompile CCNet, try again and everything’s hunky-dory.

So what is the point of all this? In my mind the GAC breaks the completeness / isolation concept for building and running an application in an environment. In my mind, I should be able to zip-up an application (as much as possible), drop it somewhere and it runs whatever the machine, given a basic set of environmental requirements. In J2EE world, when you deploy an application in an app server you put your own JAR’s in the application’s own class-path – you wouldn’t put them in the app-server’s global classpath. So (in my mind) it should be in .NET and libraries shouldn’t be in the GAC unless they are part of, or an extension of, the .NET runtime itself.

I especially don’t like that I can build something referencing a non-Runtime library in the GAC and not be given a warning.

The oft-quoted reason for using the GAC is that ‘it saves you having multiple copies of dll’s all over the place’. My response to this is that premature optimization is the root of all evil and that disk space is cheap, and the pain that shared libraries can give you does not merit the storage space / download bandwidth gain.

So in conclusion, the GAC is better than the dll-hell of COM (which thankfully I avoided by living in Java world for a few years), but still isn’t as good as not sharing library files across applications at all. My advice is don’t use the GAC unless you absolutely have to, or all the applications you use explicitally specify which versions of libraries they require.

First 36 hours in New York

I flew into New York (for the first time ever) on Thursday evening to catch up with an old friend from home who was also visiting the Big Apple. Maybe its because I’ve been in Boston for 2 months (and don’t like it hugely as a town compared with London), but I really love New York already. It seems to have lots of the great things about London and then compresses it together so you don’t have to take a 40 minute cab ride across town to get between ports of call.

So items checked off the list so-far:

– Grand Central Station

– Times Square (like Piccadilly Circus / Leicester Square on steroids)

– Jackson Hole (a damn good burger joint)

– United Nations (the cafe was shut, but I wanted to go to show my support for the organisation even if my country’s government wants to treat it with disdain)

– Empire State Building (the queues were longish but the views made it worth it)

– Staton Island ferry (which is free, and is an easy way to get a good view of the Statue of Liberty)

– Wall St (which was a lot smaller and more like London than I imagined it would be)

– Ground Zero (no comment necessary)

– various bars till 4 am

Photos to come later…

Global Underground

Global Underground have a great series of dance CD’s … which I really should start buying. I’m currently listening to #20 – Darren Emerson (ex-Underworld and all round god of a DJ.)

Going home, Chicago again and Independence Day

So having not updated my old weblog in ages, here’s what I’ve been up to recently.

Going back to London for my birthday was great – after a few weeks in a foreign land its good to see friends again. I now definitely consider London my home, which is surprising since I really didn’t enjoy it that much when I moved there.

Two weeks after getting back from London I was off to Chicago for the weekend again for a ThoughtWorks internal conference. I had a fantastic time meeting up with loads of people from work (some of whom I had met before) and enjoying the Chicago nightlife again. I’ve been to Chicago 3 times now and everytime I go I have a fab time – it reminds me a lot of London both in size/buzz and the attitude of the people that live there.

Since then I’ve just been staying around Boston. The Independence Day fireworks in Boston were very impressive and, since the weather has improved drastically in the last month, there was a huge turnout.

My plans for the next couple of months include a visit to New York next weekend, going to New Orleans with work the week after and then I’m taking 2 weeks holiday in August to hopefully travel around the ‘States a bit.

Things on my mind

There’s a few tech things I’m working on at the moment:

CruiseControl.NET is probably the thing I’m looking at most. We’re still working on a 1.0 release.

– Agile Build Engineering in general is something I want to write some stuff on. I’ve started a Wiki and Mailing List on the subject.

– The application I’m developing to generate this Blog has a bunch more of things I want to add to it.

– Thinking about Enterprise Patterns in .NET (this is something ThoughtWorks has been working with Microsoft on)

– Security still lurks at the fringes of what I’m interested in. I just bought ‘Writing Secure Code’ which is required reading at Microsoft (apparently), so that probably has cross-over with my .NET work