Comment on Reproducing the AWS Outage Race Condition with a Model CheckerparentComments−zozbot23410moThere might be plenty of potential failures that we haven't all seen, simply because the problems were fixed after TLA+ modeling brought them up.−pjmlp10moOr it might be that the model doesn't really avoid all possible human failures when translating TLA+ into Java, C++ metatemplate programming, or whatver.
Comments
There might be plenty of potential failures that we haven't all seen, simply because the problems were fixed after TLA+ modeling brought them up.
Or it might be that the model doesn't really avoid all possible human failures when translating TLA+ into Java, C++ metatemplate programming, or whatver.