[agentultra]

> Possibly formal specifications methods will improve to the point where we can reasonably use them, but we aren't there yet.

I disagree. Amazon has had great success employing TLA+ in finding bugs, testing design changes, and chasing aggressive optimizations [0].

Perhaps it is because there are myths that are still floating around regarding formal methods that still make developers cringe when they hear mention of them [1].

None the less I couldn't find reference to it in the book... did I miss it?

And besides... unit tests, I'm sure you are aware, aren't good enough alone. They can only increase your confidence in an implementation but they prove nothing.

If we want to start calling ourselves engineers I think we better start looking to how the other engineering disciplines operate. I don't think it will be long before an insurance company comes along and finds actuaries capable of monitoring risk in software development projects and liability becomes a necessary concern.

[0] http://research.microsoft.com/en-us/um/people/lamport/tla/fo...

[1] http://www.fm4industry.org/index.php/G-HM-2

[mikekchar]

I had to think about if for a bit, but you are right. My statement was waaay too general. Especially for communication protocols formal specifications are useful now. I still think we have a long way to go before we will be using tools like this every day. The main issue is whether or not it is easier to reason about the correctness of something by inspecting its design or its implementation. We can never prove that the design is correct, only that it is isomorphic to the requirements and the implementation. If there is only one document, the implementation, then the proof of isomorphism is trivial. That was my point. I personally believe that for user facing behaviour is easier and clearer to express with with tests (either integration or unit) and I really don't expect that to change in the near future.

Anyway, I regret the tone of my previous message, which mostly made me look foolish, and thank you for your kind response.

[2muchcoffeeman]

> I disagree. Amazon has had great success employing TLA+ in finding bugs, testing design changes, and chasing aggressive optimizations [0].

I googled TLA+ examples and tutorials and I am wondering how I would apply this to an already existing application?

[agentultra]

I look for the critical bottlenecks in the application where the cost of failure or mistakes is fairly high. This is where I feel I will get the most "bang for the buck" so to speak.

You don't have to specify the entire application to get the benefit of high level specifications. Even specifying the protocol between two communicating channels can bring benefits.