If you can get past Dijkstra's arrogance and abrasive presentation, he actually has some useful things to teach. If you look at one of the books where he and h

If you can get past Dijkstra's arrogance and abrasive presentation, he actually has some useful things to teach. If you look at one of the books where he and his colleagues teach how to do this (for example, A Method of Programming, by Dijkstra and Fiejen) it's pretty clear that the programmer him(her)self is supposed to come up with the formal specification. Much of the book is about how to write the specifications. The formal specifications are just assertions - they are Boolean expressions that express properties of the solution. For example the formal specification for a square root function might be abs(r*r - x) < d, where x is the number, r is the root, and d is an error tolerance. In general these formal specifications cannot be mechanically compiled into an executable program - they are nonconstructive - like the square root example above. So you still have to find or invent an algorithm. An interesting feature of Dijkstra's method is, he does suggest some heuristics for getting from the assertions to the code, that can help you discover an algorithm. They remove the mystery surrounding how some non-obvious algorithms were discovered. Dijkstra's approach is actually a lot like test-driven development - the idea is, you start with some assertions that describe what the code is supposed to do, then you check the assertions as you go -- instead of writing a bunch of code and checking it at the end. The difference is just how you check the assertions - by running tests or by attempting a proof. Test cases are formal specifications too - they are just incomplete - somebody said they are 'specification by example'.