>> Proving correctness is crucial in large systems. You can't do that... The mod... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		belter 8 months ago \| parent \| context \| favorite \| on: Systems Correctness Practices at Amazon Web Servic... >> Proving correctness is crucial in large systems. You can't do that... The model checker says the specification satisfies the properties you wrote within the finite state space you explored...

amw-zero 8 months ago [–]

You can write proofs in TLA+ and many other formalisms. You don’t need to ever use a model checker. The proofs hold for an infinite number of infinite-length executions. We are definitely not limited to finite behaviors.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact