That isn't even a good hypothesis.  Giving your developers free backrubs probably "helps build more robust, more maintainable software with fewer bugs and defects", but that doesn't make it a cost effective way of producing better software.

Formal specifications work well in rigidly defined environments (e.g. embedded/realtime systems). Here, the requirements won't change very often, since they follow from the "physical" restraints of the system.

Specification won't help much to prove the correctness of many typical "business" environments (say, a database-backed web shop that interacts with a back-end ordering service using SOAP), where large parts of the software only exists as "glue" to interact with other software, and to work around the features of third-party libraries, databases, and legacy systems. In such a system, most errors are not "business logic" errors, but "glue problems" -- the software your code interacts with doesn't work as expected (or specified).

"Specification," by definition, means "to be specific."  And therein lies the root of the problem.  

There is (and always will be) a difference between what your client wants, how well they can articulate what they want (specify), and how well you understand what is wanted.  The reason is that approximately 100% of the time, your client has no idea of what they actually need, even (especially) if they think they do.

Making a spec is fine and all, but the moment you deliver that end product to spec is the moment that either you or (more likely) your client realize that even though it's exactly what was asked for, it's not suitable to the task at hand.

A recent example? I wrote a tool to track student attendance for an Independent Study school in California. I spent 2 WEEKS going thru the whole process in intimate detail with everybody in the organization whom I could start a conversation.

I laid out a plan IN DETAIL that all parties agreed to.

I implemented said plan, over about a month. I released said plan, exactly as specified.

The VERY FIRST DAY I got a call from one of the "in charge" people who said, quite bluntly, "this will never work".

I reitereated specifications, conversations, and dates. It didn't matter. It had to change. RIGHT NOW. I spent 2.5 MONTHS cleaning up that trainwreck, until it (finally!) works smoothly and well.

I'm convinced that software CANNOT EVER be a "spec/do/finish" cycle. People, in relation to software, behave somewhat like quantum particles. Just like you cannot observe a quantum particule without changing its state, you cannot deploy software to a group of people without changing their expectations.

Software is an ITERATIVE process. Develop a methodology that rewards rapid updates and iteration, and you'll do well. Otherwise, get ready for the unemployment line!

You can manage to get a decent amount of formal specification in any language, despite it not being built into it natively. It's just a matter of having the right tools at hand. You can get a lot of mileage out of a good unit testing framework and assertion code.

As an example, I'm writing a lot of Perl these days, and among my chief weapons are Test::Class and Params::Validate. Having a large test suite written with Test::Class does wonders for formally specifying how code should behave.

When working on a module, I run the test suite associated with it every time I make a change to assure that I haven't broken everything, and prior to committing code I run the top level test suite that verifies its successful integration with everything else. This does wonders for forfending bugs. I usually catch troublesome errors before doing a commit, thus saving much heartache down the road.

As for parameter checking, Params::Validate allows me to catch all kinds of errors. Knowing up front that what is coming into your methods is as it should be allows you to focus on the internals of the method, not what is feeding it, greatly reducing the incidence rate of going barking up the wrong tree.

Of course, it is much nicer to have formal specification stuff as a native feature of the language. For example, as helpful as Params::Validate is, it is unfortunate that its behavior is not inherited by methods that override declarations in a base class. Ideally, the pre-conditions stuff would be declared in some native language construct and passed down a class hierarchy. As it stands with something like Params::Validate, you're going to end up having to cut and paste whatever you want "inherited", a highly unfortunate scenario.

My advice to anyone playing with Formal Methods is to shop around. There are MANY different methods out there, some more suited to specific types of problems than others. Don't just pick one, decide you don't like it, and avoid the whole field forever. That makes as much sense as avoiding ice cream because you don't like toffee, on the grounds that both contain sugar.

• Computer-Related Risks by Peter G. Neumann

I used to be both an avid reader and poster. I really made me appreciate the importance of quality code, with the result that over time I did what it took to make my more reliable. But it had a paralyzing effect as well: I found myself incapable of writing any code that was cheap, quick and sloppy, even if that was the best choice or what the client wanted.

-- "You're not as big an asshat as everyone seems to think." - Kurosawa Nagaya.

I can't say that I've ever rigorously specified a program I was bidding on, but I have gone some of the way there in an effort to estimate cost. Basically the problem I found was that specifying a system well enough to estimate cost with any precision was as hard as actually writing the program.

There have been several times when underbidding a consulting contract has cost me dearly.

Formal specification is definitely what you want if the cost of failure is significant. You can bet that the software the controls the space shuttle is highly specified.

By doing specification, one can write software with greater assurance that it is less buggy. But it is not a panacea: what becomes a problem in that case is when the specification is wrong. One can write the code to match the specification, but what you specified is something other than what you wanted.

-- "You're not as big an asshat as everyone seems to think." - Kurosawa Nagaya.

The bottom line is that complete formal specification and correctness proving is too expensive.   Not just expensive in terms of development cost, but in terms of market timing.

Idealists simply do not want to face the proven fact that the best code does not win in the marketplace. Instead the product that fits its niche sufficiently well first will dominate and the 'better' product will never be adopted. Shouting from the hilltop that it shouldn't be so is simply a waste of breath.  

        not def pop(empty)
        not def top(empty)
        forall s : stack; e : Elem
             · pop(push(s,e)) = s
             · top(push(s,e)) = e

While it is very precise, it is also very useless, simply because it is written in a language that 99.9% of developers do not understand. That language is also very impractical: while it is (relatively) easy to specify basic data structures and algorithms, try using it for specifying business logic. I dare you. If you even manage to do it, your specification will be:

1. Longer than the actual code
2. Completely unreadable
3. Take you forever to complete

It's all about tools. Formal specifications and proving program correctness have a great potential for improving software quality and productivity, but the tools and even the underlying theoretical analysis just isn't in place.

It is notable that Microsoft tools provide zero support and their publications about "Best Practices" don't even mention the topic. I've looked through Microsoft Research pubic websites and see precious little. Although there is a related internal MS product called 'Prefix' that is worth investigating.

One of the practical problems with software analysis tools is that you have to analyze the environment, the libraries and the operating systems as well. When the code makes a call "Outside" the analyzer gets lost. This is similar to the problem of providing symbol tables and precompiled headers for kernels and libraries -- that is, it's a solvable problem. But the whole thing requires system level support. And neither Linux nor Windows provides it.

Fortunately, there are many competing groups fighting out "Language Wars"; Python vs Ruby, C# vs Java, Lisp vs Fortran... If one of the groups could offer useful tools to provide provable practical program correctness they could pull ahead. So the question is, why aren't they doing this? Microsoft has the resources to do this and is offering nothing. The Universities and Labs have good connections with the Linux community but appear to be doing nothing. Eiffel was founded on the idea and is not exactly taking the world by storm.

The embedded systems market should be a good target for a software correctness toolset because debugging and developing can be so much more expensive in that environment. If Cisco or a telecom company is going to put a million lines of software into ROM and deploy that box to a hundred thousand remote locations you'd better believe they would be willing to spend to get it right. Likewise with avionics and some medical systems.

The market evidence is that there is something wrong with Design By Contract and proving software correct. And you can no longer claim that it's just unfamiliarity. It's been over 16 years since Gries published The Science of Programming, and 30 years since Dijkstra published A Discipline of Programming.

More importantly, Perfect Developer is an environment for writing new software. It in no way helps you write specifications and verify them on already existing code. This is a major downfall in my opinion as it is simply not feasible to throw away all the code in existance and start again with formal methods.

So what do we need? We need tools that can extract specifications from software written in existing programming languages. I'm talking C/C++, Java and to a lesser extent, Ada. A programmer can review these mechanistic specifications and refine them such that the desired behaviour of the program (not necessarily the actual behaviour) is expressed in a clear form.

Then we need automated verification tools to prove that existing software, written in the realworld programming languages I've stated above are actual refinements of the specification.

When we have these tools we will see formal methods break into the mainstream of programming, but not before.

Ok, so when's that gunna happen? 4th of Never, right? Reasoning about software is just too damn hard for a computer to do. But what about humans? Grab yourself a professor of formal methods from your local univerisity. Give him enough students and enough money and chances are he can formally prove your implementation meets your specification in a few months. How is this possible? Well duh, humans are better at symbol manipulation than computers. It's this thing we call intelligence.

How scalable is this? Assuming we had twice as many people doing formal methods could we prove a single implementation meets a single specification in a faster time? I believe we could. I believe that specifications are in fact divisible down to the statement level.. so there's no reason why throwing more adequately trained people at the problem won't result in faster formal proofs.

But that costs lots and lots of money. Where you gunna find all these people? How you gunna train them all? Professors have it easy, they have an infinite supply of first year students who have to complete their assignments to get a grade. Unfortunately he has to mark all those assignments (although automatic proof checking is a heck of a lot better than automatic proof generation) so he tends to give them all the same problem.

What if we were to start a project where people interested in formal methods could learn how to prove some open source project's source code meets its specification? We have an automated proof checker online and people submit their proof for all the different parts of the specification. We'd still have to write the specification up front, but the most time consuming part, proving the software meets the specification would be done by thousands of distributed volunteers.

Writing specifications could be a distributed activity too, but you'd have to have volunteers review the specifications written by other volunteers.

And yet most of the code that I end up writing falls into 2 categories neither of which gives to the formal specification easily -

1. Business logic. specifying it in words is already hard, coding alread complex, formal specification would be 3 to 10 times more complex than the code.

Twice more complex might still be acceptable becuase code needs more debugging than the spec.

Business logic tends to evolve over the course of project too, maintaining 3 copies of it (human language doc, formal spec and programming language code) would be a significant hindrance.

2. Libraries. once written and debugged they don't require formal specifictaion anymore. it could still be useful to verify libraries in simpler cases, like a malloc implementation, but becomes more and more difficult when higher level objects are concerned, such as an xml stream. provided that library functionality is frozen, I don't see much use in formaliszing it beyond the interface and some documentation. although I admit it would be cool!

What I would like to see on the automatic verification front is a tool that is able to deduce the intention of the programmer from the source code (with minimal annotation for the tool). so if you wrote memcmp(), it would detect a bound read-only memory access and be able to use this information later when the function is invoced from some other bit of source code. obviousely such a tool would have to come with a library of concepts it understands (such as free memory or objects or linked lists), though considering how often we reinvent the wheel in programming, I guess the variety of programming concepts is still orders of magnitude smaller than the number of implementations or pieces of code written.

Someone once wrote a demo compiler that outputs binary (for a library or function) together with a proof that the code won't do anything illegal (like reading random memory address). I suppose it cannot handle complex functions/libraries, but it's a start. And it's only a security thing, it doesn't prove the correctness of the results.