undefined | Better HN

0 pointssseveran11y ago0 comments

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

0 comments

aurelius11y ago

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.

sseveranOP11y ago

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

aurelius11y ago

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

1 more reply

j / k navigate · click thread line to collapse

0 pointssseveran11y ago0 comments

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

0 comments

aurelius11y ago

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.

sseveranOP11y ago

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

aurelius11y ago

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

1 more reply

j / k navigate · click thread line to collapse