London, fly away & formal methods

I called my friend who lives and works in London this morning to find out that he was one metro station away from one of last Thursday's blasts. He went to work 10 minutes late that morning. 10 minutes that probably saved his life. He was stuck in the underground train for two hours in the dark, with no electricity and no way out. They were two of the longest hours of his life, not knowing what was going on. After he came out, he realized that his life can be gone in a second. His wife and two girls were dead worried ofcourse, but gladly he is more than fine, and is worried that they didn't catch the perpetrators yet.

My mood today is Lenny Kravitz's song Fly Away (many thanks Jane and MMI for finding the song for me):

I wish that I could fly
Into the sky
So very high
Just like a dragonfly

I’d fly above the trees
Over the seas in all degrees
To anywhere I please

Let’s go and see the stars
The milky way or even mars
Where it could just be ours

Let’s fade into the sun
Let your spirit fly
Where we are one
Just for a little fun
Oh oh oh yeah !

I want to get away
I want to fly away
Yeah yeah yeah

I was planning to go alone to Iraq's Nassir Shamma's Oud show tonight in the club, but a friend of mine decided to join me there. I love Oud, but I'm not particularly a fan of Shamma. He's too inventive (fattay) and likes to add this philosophical themes to his pieces, naming each piece, and always gives a talk before playing each one. Just play the damn music and let me enjoy it my own way. Even a Farid Atrache's masterpiece, he had to play it in his own unique way. I like the more traditional way of playing Oud.

It was nice though still. I wasn't in the mood for Oud actually, more into Lenny's "Fly Away", so I sat on that comfy couch going through a book that my friend brought with him; The way of Z: Practical programming with formal methods

I'm afraid that my time away from the field is getting longer, but the book made me happy that I'm coming back.

They jumped from B and C languages right to Z. But Z is not a programming language, but an abstract formal specifications language. It models a system by representing its state. Novices find the appearance of Z intimidating; a mixture of boxes, text, Greek letters, and invented pictures. I think formal methods is the way to go, and the best way to describe a system to be built avoiding any ambiguities. What you would describe in 10 lines in a natural language such as English, Z would do it in one line without any ambiguity. Without complete and accurate specifications of a system, the user won't really know what he'll be getting. Z is the way to go, especially with safety-critical systems, where an error resulting from ambiguous specifications cannot be tolerated, otherwise resulting in human losses.

Looks like I might be using some of that good stuff in my new job. As I told my friend, I'm getting into this new job with a new approach; "Management doesn't matter!"