But you can see where Alan Kay's "nano-Dijkstras" joke comes from, e.g. "the horrendous mess produced by a group of incompetent, unorganized programmers", referring to your complex project.

Industry - and you - and me - have accepted that things don't always work perfectly. Industry pays people to fix things, rather than make them perfect in the first place. Partly it's an acceptance of human error; though it's also an acceptance that you'll need to change it even if it's perfect, because the world keeps changing. "Iterative development" elevates this to a dogma.

Here's a thought experiment: imagine you need a library (e.g. for network protocols; or a fancy GUI; or to parse a EDI transactions). You have a choice of two libraries. Both have been used extensively by others, and both work well when you try them out. One is proven (in Dijsktra's sense) and one is not.

1. How much more will you pay for the proven one? 10%? x2? x10? x100?

2. Now consider how much extra work was required to rigorously build the proven one. (Of course, if the builder of the component also had access to proven sub-components, this would be easier).

[You can imagine doing this by building it yourself if you like - using dollars just makes it clearer.]

If the rate of complexity increase itself increases (i.e. accelerates), then we might need a a different methodology altogether, such formal verification as you suggest. However, we have had the need for better ways to handle complexity since before Fred's Mythical Man-month (IBM 360), and we've had the tool of formal verification techniques to do it for a long time. It hasn't happened yet, suggesting there is some problem with it.

In my admittedly very limited experience of formal verification, it makes problems more complex, rather than less (This is why Dijkstra says that you can't prove software the way it is currently written - you have to write it in a simpler way, with clearer interactions between modules and so on). Its benefit is that you know it's 100% correct (assuming your assumptions, understanding of the real-world problem, understanding of interactions with other components are all correct, your proof is correct, and any proof automation tools you use are also 100% correct). OK, it gives you a higher probability that it is correct.

Ah, this looks like the opposite cause and effect from your suggestion (that formal methods are a way to handle complexity), and instead that trying to formally verify applications forces us to write them in a simpler way, which is... simpler. Or, we could just write them in a simpler way, and not worry about the formal verification part. It still leaves the problem: what is this way of writing apps in a simpler way? Isn't the only way to do this by dividing it into abstractions with well-defined behaviours and clear interfaces? In other words: Historically, we SOTSOG - using abstractions, so complexity is pushed down to a lower layer (language, libraries, OS).

PS: I would love it if there was a new general way to approach complexity. But as Fred said, "no silver bullet".

"better models for development that allow us to think about problems more abstractly"

That's possible I guess; but I don't think we lack in our ability to think about problems abstractly. It's finding the right abstraction that is tricky, and this amounts to a search through the space of abstractions. That sounds straightforward to automate, except that he search space increases exponentially with the complexity of the problem. So we need a heuristic to guide that search.

So far, the best heuristic is us. If we can automate this guide through the search space - the ability to make connections, have intuitions and insights - it would be a huge leap towards Strong AI. My Masters was an approach to this, and the start of my PhD. Quite possible, I think, but hard.

I guess my point was that in order to for larger and larger abstractions to be implemented, there needs to be trust in those abstractions. One problem that you point out is that right abstractions can be difficult to come up with, which will not be improved by formal analysis. The other problem is that as you build greater and greater abstractions on top of each other, "holes" in those abstractions can cause odd problems in the system. Here, formal verification can at least provide the level of trust that the abstraction works exactly how you expect it to and can implement your system on top of it without concern for odd effects.

One analogy could be with the computer hardware on which software is implemented upon. It goes without saying that while software is often expected to have flaws, the hardware is essentially assumed to be flawless for all intensive purposes. This isn't a perfect analogy because you have firmware, etc, but hopefully it illustrates my point. You don't worry about the processor not correctly implementing

  add ax, bx

Maybe formal analysis isn't the solution to this particular problem. I do think it is important to research the topic as fully as we can to figure out if it is or isn't.

I emphasized the invention, but you're quite right that we also need the proving. I agree with your hardware example (things like the Pentium bug are rare...), but I think we similarly rely on other layers (OS, languages, libraries), though I concede with eroding confidence as we rise.

For hardware, it's also that we have more trust in the common pathways (Dijkstra wouldn't like it - it all should be perfect. I can relate to this, but that's not how it is - today, anyway). Popular hardware is used extensively, and very importantly, I think it tends to be designed to be pretty flat, in that almost all of it gets exercised by almost all uses (i.e. there are few rare pathways). So flaws will show up quickly.

We also don't worry about the language not correctly implementing

   a+b

Concessions: Dr. Gosling apparently did write some (informal) proofs for Java, but it was in the byte-code verifier, not for the typical language stuff. But I've heard that Intel does some formal verification :-).

I agree that formal analysis is a worthwhile endeavour. I just wish they would do more work on interesting, useful problems. It used to be that computer scientists would invent something incredibly cool (like Boyer-Moore substring matching, or arithmetic coding), and then also prove it (well, really, prove some specific qualities about it). But these days, there seems to be a lot of proving things just because they can be proven - not because they are worthwhile proving. It's quite... insular.

They focus on proof, not invention.

regarding point 2: from my experience of the usefulness of formal methods (not as an afterthought--mind you!) does not necessarily imply a significant draw back on productivity, one must not forget that the proven one fares much better with testing/debugging/xyz that is a posteriori assurance. (this holds for your non-gui examples; gui programming always stuck me as a largely unsientific enterprise--probably proven by the code generated by gui builders [i have not checked in a long time, my experience is from jbuilder 4.0, which i hated anyways])

since you mentioned alan kay, you are probably interested in his recent work at vpri--check it out, there are some interesting papers and also a very good video at intel berkeley research lab: 1) http://www.vpri.org 2) http://irbseminars.intel-research.net/AlanKay.wmv

but a simple "productivity formal methods" query on scholar.google.com gives me: "Productivity on the project was the same or better than on comparable projects" pg 628/3, left column, second paragraph; by E.M. Clarke et al., "Formal methods: State of the art and future directions", 1996.

i think that you mean that developing systems, i.e., the programming part, is less productive using formal methods; which may very well be. but the additional time you lose because of debugging/testing you do not (or at least should not have to) need to spend on the formally correct system--given that the specifications were correct (this moves the source of error to a higher level)

EDIT: * none meaning no specific figures.

Some nice thoughts in Clarke (1996), p. 638 (page 13 of the pdf) http://www-2.cs.cmu.edu/~emc/papers/Papers%20In%20Refereed%2...

They would routinely use tools such as model and proof checkers with as much ease as they use compilers.

Wing [1985] envisioned over ten years ago the idea of specification firms, analogous to architecture and law firms, whose employees would be hired for their skills in formal methods.

EDIT could you share your experience, sans figures?

* model checking (error-detection/bug-discovery by using temporal logic formulas)

* interactive theorem proving (e.g. the coq-based work on verification of compilers of xavier leroy at inria, various isabelle based research projects, e.g. tum.de, cam.ac.uk, and twelf/nuprl at cmu/cornell), by formalizing denotational/operational semantics

* program correctness, axiomatic semantics (hoare triples)

using model checkers is usually a good idea if you can specify correctness properties in temporal logic formulas. i once wrote a simple and small quantification-based dsl where programmers could provide boolean predicates and set-generating functions and domain-experts would encode domain/system properties that were automatically checked or even triggered follow-up actions. i once attended a lecture given by gerard berry of esterel technologies (they do a lot of verification for airbus) and AFAIR according to him there will actually be dedicated "verification engineers" specifying formulas that ensure system correctness. using systems that support counter-example guided abstraction refinement (CEGAR, helmut veith et al.) one can iteratively develop from imprecise abstractions.

iterative theorem proving is where i think the most important work is going on, albeit (in my perception) in an orthogonal different way. in a complex system, like a compiler for a non-toy language, correctness is one of the most important problems (e.g., in the embedded systems market, automotive industry, etc.). the german research fund is doing a lot of things here, previously verifix, now a research project named verisoft. the french are very active, too. i am not sure about the situation in north america, though. in the course on verification of compilers, our lecturer told us that many companies in mechanical engineering were not really concerned with performance but rather about compilation being erroneous (one could check the bug-databases of the common compilers for reassurance on that one) i think there will be a lot of job opportunities in the future in this market, where by means of formalizing domain knowledge/programming languages one could ensure system correctness. currently, the security related industries are champions here, but with the emerging proliferation of computing technology i can imagine a world where people are fed up with badly written software, which will force engineering to verify at least certain properties.

and last but not least, while i think that axiomatic semantics are important, i think it is almost always too time consuming to write hoare triples. i have "the science of programming" by david gries, which should help my incompetent brain to speed up here, but the truth is: it's non-trivial for many programs. this is why i feel that many things are going the "interactive theorem proving"-way.

this sums it up pretty much for me. please note that i am not an expert on these issues--though very interested. axiomatic semantics and interactive theorem proving as mentioned above are not mutually exclusive, i.e., i think that one should very well be able to ensure correctness via hoare triples proven in interactive theorem provers.

"Iterative" theorem proving (though probably a typo for "interactive"), is the way this could go: "agile theorem proving". That is, where you don't need to plan ahead.

i can imagine a world where people are fed up with badly written software, which will force engineering to verify at least certain properties.

Historically, people consistently choose features, convenience and performance over well-written software. It seems that formal methods only get a foothold where there are serious consequences for failure - often legal ones.

BTW: The US/UK vs. Germany/France in computer science seems to me (from reading papers) to be pragmatism vs. theory. Reading on electromagnetism, Lord Kelvin took French scientists to task to task for their errors traceable to their algebraic and abstract methods - so this divide seems to go back a ways.

Formal analysis is a very hard -- maybe impossible -- problem for anything but toy applications. And I think it is an worthy goal to attempt to achieve, but it will not be well-served by denigrating the work of the many dedicated and intelligent "Software Engineers".

All these industries have one thing in common - a lot of money to throw around. So the technology and techniques are there, they just have to be brought down to the masses. There are signs of that happening, it just may take more time than you expect.

Like I said, I think formal analysis of software development is a laudable goal that should be pursued. But in many ways, software is so much more complex than other engineering fields that it becomes increasingly difficult if the development is not carefully controlled (something that Dijkstra is a big believer in). I know that Dijkstra recognizes that it is not an easy problem to solve, and that he feels that computer scientists have not adequately researched this area. My main point was more about his general attitude to computer engineers than to his actual point.

He addresses this well in this EWD Manuscript:

http://www.cs.utexas.edu/~EWD/transcriptions/EWD13xx/EWD1304...

But I digress, I think in the next few years as functional languages become more mainstream we'll see a huge uptake in formal methods. Not end to end mind you, but of the low level proover type tools.

Formal project planning and design languages still take too much training to be widely accepted. Can you imaging a ruby hacker analyzing and writing up his code in Z language before they code? Neither can I. But any amount of progress on this front is a good thing.

  "It is not the task of the University to offer what 
   society asks for, but to give what society needs.
   
  [The things society asks for are generally understood,
   and you don't need a University for that; the university
   has to offer what no one else can provide.]"

Hallelujah, old friend - speak the word.