OPERATIONAL DEFECT DATABASE
...
...
Among TLA+ experts, the word "prove" means to write a formal proof and check it with the TLA+ Proof System (TLAPS). We don't do that at MongoDB, we just model-check our TLA+ specs. So let's avoid saying we "prove" our specs are correct, we only "check" them.
xgen-internal-githook commented on Fri, 22 Nov 2024 22:46:04 +0000: Author: {'name': 'A. Jesse Jiryu Davis', 'email': 'jesse@emptysquare.net', 'username': 'ajdavis'} Message: SERVER-97559 Don't say we prove our TLA+ specs are correct (#29488) GitOrigin-RevId: 27a5342a5e0c92458c3447b4a0739aae82cd8809 Branch: master https://github.com/mongodb/mongo/commit/7c982b82dfa91d5e5597359adf86ca43f6e67cd9
Click on a version to see all relevant bugs
MongoDB Integration
Learn more about where this data comes from
Bug Scrub Advisor
Streamline upgrades with automated vendor bug scrubs
BugZero Enterprise
Wish you caught this bug sooner? Get proactive today.
