Formal Methods - Considered Harmful
There are lots of different formal methods.
Hang on... consider that statement. There are lots of different computer
languages, and most people outside of institutional care would readily accept
that most of those languages do pretty much the same things. A formal method is much
more abstract than a computer language : so why are there so many ? Why didn't
the second* one invented just get extended ad infinitum as new concepts were
required?
Because there's a basic misunderstanding going on here : people keep
obstinately thinking that the purpose of formal methods is improve software
production. Bzzzzt - wrong. The purpose of formal methods is to sell
books and training courses.
I think that bears repeating.
The purpose of formal methods is to sell books and training
courses.
When you understand this simple fact, it becomes obvious why there are so
many formal methods. I can't sell my books and training courses if my method is
the same as yours, so I have to dream up more symbols to join boxes with, invent
yet another name for state transition whoosits and entity relationship whatevers,
so I can copyright the stuff and take my rightful place on the gravy train.
Now I can already hear the people at the back murmuring "if there wasn't
a market for this stuff, it would rapidly die right ? So you must be wrong Bob -
by the way what time does the bar open ?". Push from the authors can't do
the job on its own - of course there is pull as well. But the pull is
also specious. Formal methods are sold to managers with two promises, which can
usefully be classified as follows :
<public> Software development speed and quality will improve !
<sub-text> Software development is easier, so you can employ cheap
bozos instead of uppity expensive programmers !
Managers of software departments are basically paranoid. That's not a
disorder, it's a rational reaction to impossible timescales and massively
variable requirements. It's not diseased to be paranoid when they really are
out to get you : and the department manager is going to carry the can when the
next disaster happens (God knows we can't have directors being to blame, so it
must be the manager, right?).
A drowning man will grasp at any straw, so if someone comes along and tells
him that his timescales will go down, then tells him quietly in the bar
afterwards that he could even consider outsourcing development to Elbonia
because the Qwizziwig formal method makes smart engineers
not-quite-so-necessary... well who wouldn't grasp that straw ?
I have seen projects using formal methods produce horrendously buggy code,
and after twenty five years and several generations of formal ballyhoo, am yet
to see any project meaningfully benefit from them.
If you really want to make a change that improves code and shortens
timescales, then you should just implement proper design reviews.
Sadly, they're in the public domain. So there's my ticket on the gravy train
gone.
opinions page
* obviously not the first, because no right-minded engineer
ever uses their first attempt at anything