In a formal state of mind.

In the Software Engineering Processes class there is a half-a-class section where they briefly mention formal methods. I tell you this so you can better understand my delusions. In that half-a-class they basically tell you formal methods is where you use a formal mathematical language to help specify software requirements. It’s very difficult and takes specialized training that the majority of software engineers do not possess. Due to the difficulty and specialized skill set required to build software with formal methods it tends to be very expensive. The take away from the lecture is that only applications where correctness of the application is critical – absolutely critical - warrant formal methods. Applications where people will die and I mean lots of people will die. Things like aircraft controller software, perhaps nuclear power plant systems, IMPORTANT STUFF.

Fast forward to the formal methods class I’m taking this semester. Like all good textbooks, the book we’re using constructs simple example situations to illustrate the points it’s trying to make. A recurring example it uses is specifying the software to run the box office of a local theater. I keep trying to reconcile what I learned in Software Engineering Processes – that only applications that result in grave lost of life require formal methods - with the needs of the local theater. The result is an ultra-violent fantasy world that I occasionally slip off into during class.

The only way I can make sense of it is if the local theater accidently sells the same seat to two different people then theater will result in a Quentin Tarantino like battle that will consume all the patrons. In short – a massacre ensues. Having identified the catastrophe that necessitates the use of formal methods I’m left to imagine the exact series of events that ignites the theater wide carnage. I assume all the patrons must be carrying weapons….otherwise it would result in a brawl, not a bloodbath…so I figure either ninjas or pirates must be involved. I favor pirates. They have a reputation for drinking, so it makes more sense that a silly thing like a double booked seat could quickly get out of hand. Of course if the double booking marred a ninja’s honor that might be cause for wonton fighting….

I got it. I expect a ninja and a pirate were both issued the same seat. The pirate, being thoroughly inebriated (i.e. a pirate) was belligerent and offended the ninja’s honor. A fight ensued. Once a fight breaks out other pirates can’t help but to join in. The pirates would probably punch the closest ninja…pretty soon the entire theater would be demolished. Oh formal methods, help us prevent this awesome series of events.