Hacker News Reader

If you have not used a model checker you don't have a proof. Please don't say that you have one. You are just hoping for the best.

See this to get yourself started: http://research.microsoft.com/en-us/um/people/lamport/tla/by...

View on HN

If you have used a model checker, you probably don't have a proof either. You have a model that might not be accurate, and testing all its inputs may be combinatorially prohibitive.

thats not the real issue. The issue with model checkers is verifying that production code actually exactly implements the model.

Yes, that is <i>another</i> issue with model checkers. Either way, your original comment is still nonsense.

No. No it is not. See the Amazon paper if you want an overview.

Reply on news.ycombinator.com