Edsger W. Dijkstra: Answers to questions from students of Software Engineering

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.

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...