However that doesn't mean I completely disagree with Lamport's arguments. Specifications are necessary in large-scale software because otherwise you can't know if you have actually implemented everything the program is supposed to do. When you release it the end-users get angry and insist that they told you in that email / meeting / watercooler conversation last year how important it was that the program frobnicate the warbles.
Lamport makes much of formal specifications. I agree that in some cases they do add value; trying to prove the correctness of a distributed protocol in any other way is dumb. But in my experience once you get up into application-level requirements a formal specification is basically source code you don't know how to compile; there is no formal correctness criteria against which you can verify it, and the stakeholders can't understand it in order to verify it.
http://paulspontifications.blogspot.co.uk/2013/01/software-h...
TL;DR: Source code is the blueprint for software.
However that doesn't mean I completely disagree with Lamport's arguments. Specifications are necessary in large-scale software because otherwise you can't know if you have actually implemented everything the program is supposed to do. When you release it the end-users get angry and insist that they told you in that email / meeting / watercooler conversation last year how important it was that the program frobnicate the warbles.
Lamport makes much of formal specifications. I agree that in some cases they do add value; trying to prove the correctness of a distributed protocol in any other way is dumb. But in my experience once you get up into application-level requirements a formal specification is basically source code you don't know how to compile; there is no formal correctness criteria against which you can verify it, and the stakeholders can't understand it in order to verify it.