That's a great editorial. The gap between IT departments and their users, and the total lack of effective communication, isn't anything new but it does seem to be affecting more and more companies.
Phil doesn't mention that's there's often also a gap and communications barriers between an IT operations department and the IT development department, and that's all part of the same problem.
Sometimes too (more often than I like) there's a similar gap between DBAs and application programmers.
Maybe it is a sympton of overspecialisation - no generalists who can see both sides of the picture?
I just saw this article in an ACM newsletter, and am now wondering if this would serve to widen the gap or shrink it?
Well, it took them somewhere between 30 and 60 man years (different amounts of effort and even different elapsed times in different reports) to get 7500 lines of verified code. The effort required is probably an exponential function of the amount of code. So if people start insisting on doing this with everything, in the present state of the art, the gap will widen quite dramatically, because there aren't enough people to do the work. Another worry is that few CS degree courses (and, I think, no IT degree courses) impart even the first clue about formal methods to their students.
In a few more years (maybe a few more decades) formal methods will become more efficient, more usable (it has taken about 35 years to get from first steps to where we are today). Maybe we will start using higher-level, less procedural and more declarative languages which allow easier analysis and proofs. But I won't hold my breath - I expect people will still be using shaky low-level languages like C and singing the praises of unblievably bad languages like C++ long after I'm dead.
And there is a real killer: for big systems we first need to prove formally that the specification is actually what we want, ie that there are no bugs in the specification. Proving that the code meets the specification isn't terribly helpful when the specification itself is full of bugs. And of course it isn't possible to achieve a formal proof unless the specification itself is formally analysable.
There have been quite a few attempts at formal specification and an awful lot of words written about them. But almost all of them have gone the way of VDM: they have become hackers' paradises, and largely drifted out of use. The only one I know of that has been used successfuly for fairly large projects (real life industrial projects, not just experiments in the lab) and is still going strong is Z (), but so far as I know it hasn't been used to get complete formal proofs - just to get a lot closer to that than pretty much anything else manages.
So I'm still very sceptical about building a complete formal proof that software works for large pieces of software with non-trivial specifications any time in the near future.